# HG changeset patch
# User wenzelm
# Date 1515334320 -3600
# Node ID f834d6f21c5525d7ade4403f2f7ca4b469933829
# Parent  fbc31dea36fac54d436e4305ad3b5420b00f6331
clarified modules;

diff -r fbc31dea36fa -r f834d6f21c55 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sun Jan 07 14:48:54 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Jan 07 15:12:00 2018 +0100
@@ -34,6 +34,7 @@
   val scan_cartouche: string -> T list -> T list * T list
   val scan_cartouche_content: string -> T list -> T list * T list
   val recover_cartouche: T list -> T list * T list
+  val scan_comment_cartouche: string -> 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
@@ -215,6 +216,11 @@
 
 val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
 
+fun scan_comment_cartouche err_prefix =
+  $$$ Symbol.comment @@@ Scan.many (Symbol.is_blank o symbol) @@@
+  !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote Symbol.comment)
+    (scan_cartouche err_prefix);
+
 
 (* ML-style comments *)
 
diff -r fbc31dea36fa -r f834d6f21c55 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Jan 07 14:48:54 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Jan 07 15:12:00 2018 +0100
@@ -246,12 +246,6 @@
 val explode_str = explode_literal scan_str_body;
 
 
-(* comment cartouche *)
-
-val scan_comment_cartouche =
-  $$$ "\<comment>" @@@ Scan.many (Symbol.is_blank o Symbol_Pos.symbol) @@@
-    !!! "cartouche expected after \"\<comment>\"" (Symbol_Pos.scan_cartouche err_prefix);
-
 
 (** tokenize **)
 
@@ -278,7 +272,7 @@
     val scan_token =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
       Symbol_Pos.scan_comment err_prefix >> token Comment ||
-      scan_comment_cartouche >> token Comment_Cartouche ||
+      Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment_Cartouche ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token StringSy ||
       scan_str >> token StrSy ||