more precise Symbol_Pos.quote_string;

--- a/src/Pure/General/symbol_pos.ML	Tue Jul 12 13:45:05 2011 +0200
+++ b/src/Pure/General/symbol_pos.ML	Tue Jul 12 14:33:08 2011 +0200
@@ -19,6 +19,9 @@
   val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
   val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
   val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
+  val quote_string_q: string -> string
+  val quote_string_qq: string -> string
+  val quote_string_bq: string -> string
   val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
     T list -> T list * T list
   val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
@@ -75,7 +78,7 @@
 val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
 
 
-(* Isabelle strings *)
+(* scan string literals *)
 
 local
 
@@ -104,6 +107,29 @@
 end;
 
 
+(* quote string literals *)
+
+local
+
+fun char_code i =
+  (if i < 10 then "00" else if i < 100 then "0" else "") ^ string_of_int i;
+
+fun quote_str q s =
+  if Symbol.is_ascii_control s then "\\" ^ char_code (ord s)
+  else if s = q orelse s = "\\" then "\\" ^ s
+  else s;
+
+fun quote_string q = enclose q q o implode o map (quote_str q) o Symbol.explode;
+
+in
+
+val quote_string_q = quote_string "'";
+val quote_string_qq = quote_string "\"";
+val quote_string_bq = quote_string "`";
+
+end;
+
+
 (* ML-style comments *)
 
 local

--- a/src/Pure/Isar/token.ML	Tue Jul 12 13:45:05 2011 +0200
+++ b/src/Pure/Isar/token.ML	Tue Jul 12 14:33:08 2011 +0200
@@ -191,15 +191,12 @@
 
 (* unparse *)
 
-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 o escape "\""
-  | AltString => x |> enclose "`" "`" o escape "`"
-  | Verbatim => x |> enclose "{*" "*}"
-  | Comment => x |> enclose "(*" "*)"
+    String => Symbol_Pos.quote_string_qq x
+  | AltString => Symbol_Pos.quote_string_bq x
+  | Verbatim => enclose "{*" "*}" x
+  | Comment => enclose "(*" "*)" x
   | Sync => ""
   | EOF => ""
   | _ => x);