# HG changeset patch
# User wenzelm
# Date 1390244692 -3600
# Node ID 75815b3b38a1fb03a652ef98246c842a451e6e7e
# Parent  8284c0d5bf52aee806a4e48d4cff213f4efe994b
tuned -- more direct err_prefix;

diff -r 8284c0d5bf52 -r 75815b3b38a1 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Mon Jan 20 19:47:31 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Mon Jan 20 20:04:52 2014 +0100
@@ -50,7 +50,7 @@
 
 val scan_ant =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
-  Scan.trace (Symbol_Pos.scan_cartouche (fn s => Symbol_Pos.!!! (fn () => err_prefix ^ s))) >> #2 ||
+  Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
 
 in
diff -r 8284c0d5bf52 -r 75815b3b38a1 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 19:47:31 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:04:52 2014 +0100
@@ -27,14 +27,11 @@
   val quote_string_q: string -> string
   val quote_string_qq: string -> string
   val quote_string_bq: string -> string
-  val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
-    T list -> T list * T list
+  val scan_cartouche: string -> T list -> T list * T list
   val recover_cartouche: T list -> T list * T list
   val cartouche_content: T list -> 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) ->
-    T list -> T list * T list
+  val scan_comment: string -> T list -> T list * T list
+  val scan_comment_body: string -> T list -> T list * T list
   val recover_comment: T list -> T list * T list
   val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
@@ -168,9 +165,9 @@
         $$ "\\<close>" >> pair (d - 1)
       else Scan.fail)));
 
-fun scan_cartouche cut =
+fun scan_cartouche err_prefix =
   Scan.ahead ($$ "\\<open>") |--
-    cut "unclosed text cartouche"
+    !!! (fn () => err_prefix ^ "unclosed text cartouche")
       (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
 
 val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
@@ -206,11 +203,13 @@
 
 in
 
-fun scan_comment cut =
-  $$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")");
+fun scan_comment err_prefix =
+  $$$ "(" @@@ $$$ "*" @@@
+    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body @@@ $$$ "*" @@@ $$$ ")");
 
-fun scan_comment_body cut =
-  $$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")");
+fun scan_comment_body err_prefix =
+  $$$ "(" |-- $$$ "*" |--
+    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body --| $$$ "*" --| $$$ ")");
 
 val recover_comment =
   $$$ "(" @@@ $$$ "*" @@@ scan_cmts;
diff -r 8284c0d5bf52 -r 75815b3b38a1 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Jan 20 19:47:31 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Jan 20 20:04:52 2014 +0100
@@ -337,7 +337,7 @@
 
 val scan_cartouche =
   Symbol_Pos.scan_pos --
-    ((Symbol_Pos.scan_cartouche !!! >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
+    ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
 
 
 (* scan space *)
@@ -352,7 +352,7 @@
 (* scan comment *)
 
 val scan_comment =
-  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
+  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos);
 
 
 
diff -r 8284c0d5bf52 -r 75815b3b38a1 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Jan 20 19:47:31 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Mon Jan 20 20:04:52 2014 +0100
@@ -137,7 +137,9 @@
 
 open Basic_Symbol_Pos;
 
-fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);
+val err_prefix = "SML lexical error: ";
+
+fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 
 (* blanks *)
@@ -261,7 +263,7 @@
  (scan_char >> token Char ||
   scan_string >> token String ||
   scan_blanks1 >> token Space ||
-  Symbol_Pos.scan_comment !!! >> token Comment ||
+  Symbol_Pos.scan_comment err_prefix >> token Comment ||
   Scan.max token_leq
    (scan_keyword >> token Keyword)
    (scan_word >> token Word ||
diff -r 8284c0d5bf52 -r 75815b3b38a1 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Jan 20 19:47:31 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:04:52 2014 +0100
@@ -87,7 +87,9 @@
 
 open Basic_Symbol_Pos;
 
-fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
+val err_prefix = "Inner lexical error: ";
+
+fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 val scan_id = Symbol_Pos.scan_ident;
 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
@@ -258,8 +260,8 @@
     val scan_lit = Scan.literal lex >> token Literal;
 
     val scan_token =
-      Symbol_Pos.scan_cartouche !!! >> token Cartouche ||
-      Symbol_Pos.scan_comment !!! >> token Comment ||
+      Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
+      Symbol_Pos.scan_comment err_prefix >> token Comment ||
       Scan.max token_leq scan_lit scan_val ||
       scan_str >> token StrSy ||
       Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;