more uniform variations of scan_string;
authorwenzelm
Sat Apr 30 18:16:40 2011 +0200 (2011-04-30)
changeset 4250327514b6fbe93
parent 42502 13b41fb77649
child 42504 869c3f6f2d6e
more uniform variations of scan_string;
src/Pure/General/antiquote.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Thu Apr 28 21:06:04 2011 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Sat Apr 30 18:16:40 2011 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4      andalso Symbol.is_regular s) >> single;
     1.5  
     1.6  val scan_ant =
     1.7 -  Symbol_Pos.scan_quoted ||
     1.8 +  Scan.trace (Symbol_Pos.scan_string_qq || Symbol_Pos.scan_string_bq) >> #2 ||
     1.9    Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    1.10  
    1.11  val scan_antiq =
     2.1 --- a/src/Pure/General/symbol_pos.ML	Thu Apr 28 21:06:04 2011 +0200
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Apr 30 18:16:40 2011 +0200
     2.3 @@ -17,9 +17,9 @@
     2.4    val !!! : string -> (T list -> 'a) -> T list -> 'a
     2.5    val change_prompt: ('a -> 'b) -> 'a -> 'b
     2.6    val scan_pos: T list -> Position.T * T list
     2.7 -  val scan_string: T list -> (Position.T * (T list * Position.T)) * T list
     2.8 -  val scan_alt_string: T list -> (Position.T * (T list * Position.T)) * T list
     2.9 -  val scan_quoted: T list -> T list * T list
    2.10 +  val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
    2.11 +  val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
    2.12 +  val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
    2.13    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    2.14      T list -> T list * T list
    2.15    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    2.16 @@ -112,10 +112,9 @@
    2.17  
    2.18  in
    2.19  
    2.20 -val scan_string = scan_strs "\"";
    2.21 -val scan_alt_string = scan_strs "`";
    2.22 -
    2.23 -val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
    2.24 +val scan_string_q = scan_strs "'";
    2.25 +val scan_string_qq = scan_strs "\"";
    2.26 +val scan_string_bq = scan_strs "`";
    2.27  
    2.28  end;
    2.29  
     3.1 --- a/src/Pure/Isar/token.ML	Thu Apr 28 21:06:04 2011 +0200
     3.2 +++ b/src/Pure/Isar/token.ML	Sat Apr 30 18:16:40 2011 +0200
     3.3 @@ -325,8 +325,8 @@
     3.4    Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
     3.5  
     3.6  fun scan (lex1, lex2) = !!! "bad input"
     3.7 -  (Symbol_Pos.scan_string >> token_range String ||
     3.8 -    Symbol_Pos.scan_alt_string >> token_range AltString ||
     3.9 +  (Symbol_Pos.scan_string_qq >> token_range String ||
    3.10 +    Symbol_Pos.scan_string_bq >> token_range AltString ||
    3.11      scan_verbatim >> token_range Verbatim ||
    3.12      scan_comment >> token_range Comment ||
    3.13      scan_space >> token Space ||