tuned error messages, more accurate position;

--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Jan 20 20:04:52 2014 +0100
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Jan 20 20:24:44 2014 +0100
@@ -205,7 +205,7 @@
 val any_line = whitespace' |-- any_line' --|
   newline >> (implode o map symbol);
 
-fun gen_comment a b = $$$ a |-- !!! "missing end of comment"
+fun gen_comment a b = $$$ a |-- !!! "unclosed comment"
   (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment;
 
 val c_comment = gen_comment "/*" "*/";

--- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:04:52 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:24:44 2014 +0100
@@ -204,12 +204,14 @@
 in
 
 fun scan_comment err_prefix =
-  $$$ "(" @@@ $$$ "*" @@@
-    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body @@@ $$$ "*" @@@ $$$ ")");
+  Scan.ahead ($$ "(" -- $$ "*") |--
+    !!! (fn () => err_prefix ^ "unclosed comment")
+      ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")");
 
 fun scan_comment_body err_prefix =
-  $$$ "(" |-- $$$ "*" |--
-    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body --| $$$ "*" --| $$$ ")");
+  Scan.ahead ($$ "(" -- $$ "*") |--
+    !!! (fn () => err_prefix ^ "unclosed comment")
+      ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")");
 
 val recover_comment =
   $$$ "(" @@@ $$$ "*" @@@ scan_cmts;

--- a/src/Pure/Isar/token.ML	Mon Jan 20 20:04:52 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Jan 20 20:24:44 2014 +0100
@@ -325,9 +325,11 @@
   Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
 
 val scan_verbatim =
-  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
-    (Symbol_Pos.change_prompt
-      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
+  Scan.ahead ($$$ "{" -- $$$ "*") |--
+    !!! "unclosed verbatim text"
+      ((Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") --
+        Symbol_Pos.change_prompt
+          ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
 
 val recover_verbatim =
   $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);

--- a/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:04:52 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:24:44 2014 +0100
@@ -217,12 +217,14 @@
   $$$ "'" --| Scan.ahead (~$$$ "'");
 
 val scan_str =
-  $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
-    ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
+  Scan.ahead ($$ "'" -- $$ "'") |--
+    !!! "unclosed string literal"
+      ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
 
 val scan_str_body =
-  $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
-    ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
+  Scan.ahead ($$$ "'" |-- $$$ "'") |--
+    !!! "unclosed string literal"
+      ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
 
 
 fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));