Fix to unparse to not double-escape backslash
authoraspinall
Tue Sep 28 10:43:34 2004 +0200 (2004-09-28)
changeset 15209b62f72ea3bb0
parent 15208 09271a87fbf0
child 15210 4ff917a91e16
Fix to unparse to not double-escape backslash
src/Pure/Isar/outer_lex.ML
     1.1 --- a/src/Pure/Isar/outer_lex.ML	Mon Sep 27 16:03:16 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_lex.ML	Tue Sep 28 10:43:34 2004 +0200
     1.3 @@ -142,7 +142,7 @@
     1.4  
     1.5  fun unparse (Token (_, (kind, x))) =
     1.6    (case kind of
     1.7 -    String => x |> translate_string (fn "\"" => "\\\"" | "\\" => "\\\\" | c => c) |> quote
     1.8 +    String => x |> quote
     1.9    | Verbatim => x |> enclose "{*" "*}"
    1.10    | Comment => x |> enclose "(*" "*)"
    1.11    | _ => x);