# HG changeset patch
# User wenzelm
# Date 1344630345 -7200
# Node ID 4fe0920d5049effa6fd61cf648338084542ff780
# Parent  de68fc11c2456a5d4e4118c6a7315856b2890673
proper error prefixes;

diff -r de68fc11c245 -r 4fe0920d5049 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Fri Aug 10 21:53:20 2012 +0200
+++ b/src/Pure/General/antiquote.ML	Fri Aug 10 22:25:45 2012 +0200
@@ -67,13 +67,15 @@
 
 local
 
+val err_prefix = "Antiquotation lexical error: ";
+
 val scan_txt =
   $$$ "@" --| Scan.ahead (~$$$ "{") ||
   Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
     andalso Symbol.is_regular s) >> single;
 
 val scan_ant =
-  Scan.trace (Symbol_Pos.scan_string_qq || Symbol_Pos.scan_string_bq) >> #2 ||
+  Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
 
 val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
@@ -83,7 +85,7 @@
 
 val scan_antiq =
   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
-    Symbol_Pos.!!! (fn () => "missing closing brace of antiquotation")
+    Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
   >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 
diff -r de68fc11c245 -r 4fe0920d5049 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Fri Aug 10 21:53:20 2012 +0200
+++ b/src/Pure/General/symbol_pos.ML	Fri Aug 10 22:25:45 2012 +0200
@@ -16,9 +16,9 @@
   val !!! : Scan.message -> (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_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_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list
+  val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list
+  val scan_string_bq: string -> T list -> (Position.T * (T list * Position.T)) * T list
   val recover_string_q: T list -> T list * T list
   val recover_string_qq: T list -> T list * T list
   val recover_string_bq: T list -> T list * T list
@@ -94,16 +94,17 @@
     let val (n, _) = Library.read_int [a, b, c]
     in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
 
-fun scan_str q =
-  $$$ "\\" |-- !!! (fn () => "bad escape character in string") ($$$ q || $$$ "\\" || char_code) ||
+fun scan_str q err_prefix =
+  $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string")
+    ($$$ q || $$$ "\\" || char_code) ||
   Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
 
-fun scan_strs q =
-  (scan_pos --| $$$ q) -- !!! (fn () => "missing quote at end of string")
-    (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
+fun scan_strs q err_prefix =
+  (scan_pos --| $$$ q) -- !!! (fn () => err_prefix ^ "missing quote at end of string")
+    (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
 
 fun recover_strs q =
-  $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q)) >> flat);
+  $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
 
 in
 
diff -r de68fc11c245 -r 4fe0920d5049 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Aug 10 21:53:20 2012 +0200
+++ b/src/Pure/Isar/token.ML	Fri Aug 10 22:25:45 2012 +0200
@@ -273,7 +273,9 @@
 
 open Basic_Symbol_Pos;
 
-fun !!! msg = Symbol_Pos.!!! (fn () => "Outer lexical error: " ^ msg);
+val err_prefix = "Outer lexical error: ";
+
+fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 
 (* scan symbolic idents *)
@@ -342,8 +344,8 @@
   Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
 
 fun scan (lex1, lex2) = !!! "bad input"
-  (Symbol_Pos.scan_string_qq >> token_range String ||
-    Symbol_Pos.scan_string_bq >> token_range AltString ||
+  (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
+    Symbol_Pos.scan_string_bq err_prefix >> token_range AltString ||
     scan_verbatim >> token_range Verbatim ||
     scan_comment >> token_range Comment ||
     scan_space >> token Space ||
diff -r de68fc11c245 -r 4fe0920d5049 src/Pure/Thy/rail.ML
--- a/src/Pure/Thy/rail.ML	Fri Aug 10 21:53:20 2012 +0200
+++ b/src/Pure/Thy/rail.ML	Fri Aug 10 22:25:45 2012 +0200
@@ -63,16 +63,18 @@
 val scan_keyword =
   Scan.one (member (op =) ["|", "*", "+", "?", "(", ")", "\\", ";", ":", "@"] o Symbol_Pos.symbol);
 
+val err_prefix = "Rail lexical error: ";
+
 val scan_token =
   scan_space >> K [] ||
   Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||
-  Symbol_Pos.scan_string_q >> (token String o #1 o #2);
+  Symbol_Pos.scan_string_q err_prefix >> (token String o #1 o #2);
 
 val scan =
   (Scan.repeat scan_token >> flat) --|
-    Symbol_Pos.!!! (fn () => "Rail lexical error: bad input")
+    Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
       (Scan.ahead (Scan.one Symbol_Pos.is_eof));
 
 in