--- a/src/Pure/General/antiquote.ML Thu Apr 28 21:06:04 2011 +0200
+++ b/src/Pure/General/antiquote.ML Sat Apr 30 18:16:40 2011 +0200
@@ -72,7 +72,7 @@
andalso Symbol.is_regular s) >> single;
val scan_ant =
- Symbol_Pos.scan_quoted ||
+ Scan.trace (Symbol_Pos.scan_string_qq || Symbol_Pos.scan_string_bq) >> #2 ||
Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
val scan_antiq =
--- a/src/Pure/General/symbol_pos.ML Thu Apr 28 21:06:04 2011 +0200
+++ b/src/Pure/General/symbol_pos.ML Sat Apr 30 18:16:40 2011 +0200
@@ -17,9 +17,9 @@
val !!! : string -> (T list -> 'a) -> T list -> 'a
val change_prompt: ('a -> 'b) -> 'a -> 'b
val scan_pos: T list -> Position.T * T list
- val scan_string: T list -> (Position.T * (T list * Position.T)) * T list
- val scan_alt_string: T list -> (Position.T * (T list * Position.T)) * T list
- val scan_quoted: T list -> T list * T list
+ 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 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) ->
@@ -112,10 +112,9 @@
in
-val scan_string = scan_strs "\"";
-val scan_alt_string = scan_strs "`";
-
-val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
+val scan_string_q = scan_strs "'";
+val scan_string_qq = scan_strs "\"";
+val scan_string_bq = scan_strs "`";
end;
--- a/src/Pure/Isar/token.ML Thu Apr 28 21:06:04 2011 +0200
+++ b/src/Pure/Isar/token.ML Sat Apr 30 18:16:40 2011 +0200
@@ -325,8 +325,8 @@
Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
fun scan (lex1, lex2) = !!! "bad input"
- (Symbol_Pos.scan_string >> token_range String ||
- Symbol_Pos.scan_alt_string >> token_range AltString ||
+ (Symbol_Pos.scan_string_qq >> token_range String ||
+ Symbol_Pos.scan_string_bq >> token_range AltString ||
scan_verbatim >> token_range Verbatim ||
scan_comment >> token_range Comment ||
scan_space >> token Space ||