# HG changeset patch
# User wenzelm
# Date 1390233378 -3600
# Node ID 57d87ec3da4cbbbe6bd9f011c287fa07d129828d
# Parent  f69530f22f5a27a6a054c6875ca3598024728765
tuned errors;

diff -r f69530f22f5a -r 57d87ec3da4c src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 16:14:19 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 16:56:18 2014 +0100
@@ -8,6 +8,7 @@
 sig
   type T = Symbol.symbol * Position.T
   val symbol: T -> Symbol.symbol
+  val $$ : Symbol.symbol -> T list -> T * T list
   val $$$ : Symbol.symbol -> T list -> T list * T list
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
   val content: T list -> string
@@ -115,8 +116,10 @@
   Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
 
 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)));
+  Scan.ahead ($$ q) |--
+    !!! (fn () => err_prefix ^ "unclosed string literal")
+      ((scan_pos --| $$$ q) --
+        (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);
@@ -284,6 +287,7 @@
 
 structure Basic_Symbol_Pos =   (*not open by default*)
 struct
+  val $$ = Symbol_Pos.$$;
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;
diff -r f69530f22f5a -r 57d87ec3da4c src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Jan 20 16:14:19 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Jan 20 16:56:18 2014 +0100
@@ -116,10 +116,10 @@
   | TypeVar => "schematic type variable"
   | Nat => "natural number"
   | Float => "floating-point number"
-  | String => "string"
+  | String => "quoted string"
   | AltString => "back-quoted string"
   | Verbatim => "verbatim text"
-  | Cartouche => "cartouche"
+  | Cartouche => "text cartouche"
   | Space => "white space"
   | Comment => "comment text"
   | InternalValue => "internal value"
diff -r f69530f22f5a -r 57d87ec3da4c src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Jan 20 16:14:19 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Mon Jan 20 16:56:18 2014 +0100
@@ -241,8 +241,9 @@
   $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) [];
 
 val scan_string =
-  $$$ "\"" @@@ !!! "missing quote at end of string"
-    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
+  Scan.ahead ($$ "\"") |--
+    !!! "unclosed string literal"
+      ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
 
 val recover_string =
   $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat);
@@ -304,9 +305,7 @@
           (SOME (false, fn msg => recover msg >> map Antiquote.Text))
         |> Source.exhaust
         |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
-        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
-      handle ERROR msg =>
-        cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
+        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
   in input @ termination end;
 
 end;