# 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);