# HG changeset patch
# User wenzelm
# Date 1304180200 -7200
# Node ID 27514b6fbe93bcfbaf1ba15c51b09db3cadb5f59
# Parent  13b41fb77649d0f4814ef1fd4935ecdb325cdff3
more uniform variations of scan_string;

diff -r 13b41fb77649 -r 27514b6fbe93 src/Pure/General/antiquote.ML
--- 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 =
diff -r 13b41fb77649 -r 27514b6fbe93 src/Pure/General/symbol_pos.ML
--- 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;
 
diff -r 13b41fb77649 -r 27514b6fbe93 src/Pure/Isar/token.ML
--- 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 ||