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