src/Pure/General/symbol_pos.ML
changeset 43773 e8ba493027a3
parent 43709 717e96cf9527
child 43947 9b00f09f7721
equal deleted inserted replaced
43772:c825594fd0c1 43773:e8ba493027a3
    17   val change_prompt: ('a -> 'b) -> 'a -> 'b
    17   val change_prompt: ('a -> 'b) -> 'a -> 'b
    18   val scan_pos: T list -> Position.T * T list
    18   val scan_pos: T list -> Position.T * T list
    19   val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
    19   val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
    20   val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
    20   val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
    21   val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
    21   val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
       
    22   val quote_string_q: string -> string
       
    23   val quote_string_qq: string -> string
       
    24   val quote_string_bq: string -> string
    22   val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    25   val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    23     T list -> T list * T list
    26     T list -> T list * T list
    24   val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    27   val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    25     T list -> T list * T list
    28     T list -> T list * T list
    26   val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
    29   val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
    73 fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
    76 fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
    74 
    77 
    75 val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
    78 val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
    76 
    79 
    77 
    80 
    78 (* Isabelle strings *)
    81 (* scan string literals *)
    79 
    82 
    80 local
    83 local
    81 
    84 
    82 val char_code =
    85 val char_code =
    83   Scan.one (Symbol.is_ascii_digit o symbol) --
    86   Scan.one (Symbol.is_ascii_digit o symbol) --
   102 val scan_string_bq = scan_strs "`";
   105 val scan_string_bq = scan_strs "`";
   103 
   106 
   104 end;
   107 end;
   105 
   108 
   106 
   109 
       
   110 (* quote string literals *)
       
   111 
       
   112 local
       
   113 
       
   114 fun char_code i =
       
   115   (if i < 10 then "00" else if i < 100 then "0" else "") ^ string_of_int i;
       
   116 
       
   117 fun quote_str q s =
       
   118   if Symbol.is_ascii_control s then "\\" ^ char_code (ord s)
       
   119   else if s = q orelse s = "\\" then "\\" ^ s
       
   120   else s;
       
   121 
       
   122 fun quote_string q = enclose q q o implode o map (quote_str q) o Symbol.explode;
       
   123 
       
   124 in
       
   125 
       
   126 val quote_string_q = quote_string "'";
       
   127 val quote_string_qq = quote_string "\"";
       
   128 val quote_string_bq = quote_string "`";
       
   129 
       
   130 end;
       
   131 
       
   132 
   107 (* ML-style comments *)
   133 (* ML-style comments *)
   108 
   134 
   109 local
   135 local
   110 
   136 
   111 val scan_cmt =
   137 val scan_cmt =