more precise Symbol_Pos.quote_string;
authorwenzelm
Tue Jul 12 14:33:08 2011 +0200 (2011-07-12)
changeset 43773e8ba493027a3
parent 43772 c825594fd0c1
child 43774 6dfdb70496fe
more precise Symbol_Pos.quote_string;
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Tue Jul 12 13:45:05 2011 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Jul 12 14:33:08 2011 +0200
     1.3 @@ -19,6 +19,9 @@
     1.4    val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
     1.5    val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
     1.6    val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
     1.7 +  val quote_string_q: string -> string
     1.8 +  val quote_string_qq: string -> string
     1.9 +  val quote_string_bq: string -> string
    1.10    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.11      T list -> T list * T list
    1.12    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.13 @@ -75,7 +78,7 @@
    1.14  val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
    1.15  
    1.16  
    1.17 -(* Isabelle strings *)
    1.18 +(* scan string literals *)
    1.19  
    1.20  local
    1.21  
    1.22 @@ -104,6 +107,29 @@
    1.23  end;
    1.24  
    1.25  
    1.26 +(* quote string literals *)
    1.27 +
    1.28 +local
    1.29 +
    1.30 +fun char_code i =
    1.31 +  (if i < 10 then "00" else if i < 100 then "0" else "") ^ string_of_int i;
    1.32 +
    1.33 +fun quote_str q s =
    1.34 +  if Symbol.is_ascii_control s then "\\" ^ char_code (ord s)
    1.35 +  else if s = q orelse s = "\\" then "\\" ^ s
    1.36 +  else s;
    1.37 +
    1.38 +fun quote_string q = enclose q q o implode o map (quote_str q) o Symbol.explode;
    1.39 +
    1.40 +in
    1.41 +
    1.42 +val quote_string_q = quote_string "'";
    1.43 +val quote_string_qq = quote_string "\"";
    1.44 +val quote_string_bq = quote_string "`";
    1.45 +
    1.46 +end;
    1.47 +
    1.48 +
    1.49  (* ML-style comments *)
    1.50  
    1.51  local
     2.1 --- a/src/Pure/Isar/token.ML	Tue Jul 12 13:45:05 2011 +0200
     2.2 +++ b/src/Pure/Isar/token.ML	Tue Jul 12 14:33:08 2011 +0200
     2.3 @@ -191,15 +191,12 @@
     2.4  
     2.5  (* unparse *)
     2.6  
     2.7 -fun escape q =
     2.8 -  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
     2.9 -
    2.10  fun unparse (Token (_, (kind, x), _)) =
    2.11    (case kind of
    2.12 -    String => x |> quote o escape "\""
    2.13 -  | AltString => x |> enclose "`" "`" o escape "`"
    2.14 -  | Verbatim => x |> enclose "{*" "*}"
    2.15 -  | Comment => x |> enclose "(*" "*)"
    2.16 +    String => Symbol_Pos.quote_string_qq x
    2.17 +  | AltString => Symbol_Pos.quote_string_bq x
    2.18 +  | Verbatim => enclose "{*" "*}" x
    2.19 +  | Comment => enclose "(*" "*)" x
    2.20    | Sync => ""
    2.21    | EOF => ""
    2.22    | _ => x);