# HG changeset patch
# User wenzelm
# Date 1310473988 -7200
# Node ID e8ba493027a3e72984b71e61a6590adab7ae4fb4
# Parent  c825594fd0c1e2c3c87452136f60c07acf29e484
more precise Symbol_Pos.quote_string;

diff -r c825594fd0c1 -r e8ba493027a3 src/Pure/General/symbol_pos.ML
--- 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
diff -r c825594fd0c1 -r e8ba493027a3 src/Pure/Isar/token.ML
--- 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);