# HG changeset patch
# User wenzelm
# Date 1136243189 -3600
# Node ID d1978038b9451502617555c8fc7345295711dbda
# Parent  d9b026de8333d327e9b9c8844c8d86af1f53f161
unparse String/AltString: escape quotes;

diff -r d9b026de8333 -r d1978038b945 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Tue Jan 03 00:06:28 2006 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Tue Jan 03 00:06:29 2006 +0100
@@ -150,10 +150,13 @@
   else if x = "" then str_of_kind k
   else str_of_kind k ^ " " ^ quote x;
 
+fun escape q =
+  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
+
 fun unparse (Token (_, (kind, x))) =
   (case kind of
-    String => x |> quote
-  | AltString => x |> enclose "`" "`"
+    String => x |> quote o escape "\""
+  | AltString => x |> enclose "`" "`" o escape "`"
   | Verbatim => x |> enclose "{*" "*}"
   | Comment => x |> enclose "(*" "*)"
   | _ => x);