src/Pure/General/symbol_pos.ML
changeset 43773 e8ba493027a3
parent 43709 717e96cf9527
child 43947 9b00f09f7721
     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