clarified modules: uniform notion of formal comments;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/comment.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -0,0 +1,73 @@
+(*  Title:      Pure/General/comment.ML
+    Author:     Makarius
+
+Formal comments.
+*)
+
+signature COMMENT =
+sig
+  datatype kind = Comment | Cancel
+  val scan_comment: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
+  val scan_cancel: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
+  val scan: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
+  val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
+end;
+
+structure Comment: COMMENT =
+struct
+
+(* kinds *)
+
+datatype kind = Comment | Cancel;
+
+val kinds =
+  [(Comment, {symbol = Symbol.comment, blanks = true}),
+   (Cancel, {symbol = Symbol.cancel, blanks = false})];
+
+val get_kind = the o AList.lookup (op =) kinds;
+val print_kind = quote o #symbol o get_kind;
+
+fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
+
+
+(* scan *)
+
+local
+
+open Basic_Symbol_Pos;
+
+val err_prefix = "Error in formal comment: ";
+
+val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
+
+fun scan_symbol kind =
+  let val {blanks, symbol} = get_kind kind
+  in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
+
+fun scan_strict kind =
+  scan_symbol kind @@@
+    Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind)
+      (Symbol_Pos.scan_cartouche err_prefix) >> pair kind;
+
+fun scan_permissive kind =
+  scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >>
+    (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss));
+
+in
+
+val scan_comment = scan_strict Comment;
+val scan_cancel = scan_strict Cancel;
+val scan = scan_comment || scan_cancel;
+
+val scan_body =
+  Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
+  scan_permissive Comment || scan_permissive Cancel;
+
+fun read_body syms =
+  if exists (is_symbol o Symbol_Pos.symbol) syms then
+    Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
+  else NONE;
+
+end;
+
+end;

--- a/src/Pure/General/symbol_pos.ML	Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -34,9 +34,6 @@
   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_blanks: T list -> T list * T list
-  val scan_cancel_cartouche: string -> 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
@@ -219,19 +216,6 @@
 val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
 
 
-(* operator with cartouche argument *)
-
-val scan_blanks = Scan.many (Symbol.is_blank o symbol);
-
-fun scan_operator_cartouche blanks operator_symbol err_prefix =
-  (if blanks then $$$ operator_symbol @@@ scan_blanks else $$$ operator_symbol) @@@
-    !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote operator_symbol)
-      (scan_cartouche err_prefix);
-
-val scan_cancel_cartouche = scan_operator_cartouche false Symbol.cancel;
-val scan_comment_cartouche = scan_operator_cartouche true Symbol.comment;
-
-
 (* ML-style comments *)
 
 local

--- a/src/Pure/ML/ml_lex.ML	Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -9,7 +9,7 @@
   val keywords: string list
   datatype token_kind =
     Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
-    Space | Comment | Comment_Cartouche | Error of string | EOF
+    Space | Comment of Comment.kind option | Error of string | EOF
   eqtype token
   val stopper: token Scan.stopper
   val is_regular: token -> bool
@@ -64,7 +64,7 @@
 
 datatype token_kind =
   Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
-  Space | Comment | Comment_Cartouche | Error of string | EOF;
+  Space | Comment of Comment.kind option | Error of string | EOF;
 
 datatype token = Token of Position.range * (token_kind * string);
 
@@ -108,12 +108,10 @@
   | is_regular _ = true;
 
 fun is_improper (Token (_, (Space, _))) = true
-  | is_improper (Token (_, (Comment, _))) = true
-  | is_improper (Token (_, (Comment_Cartouche, _))) = true
+  | is_improper (Token (_, (Comment _, _))) = true
   | is_improper _ = false;
 
-fun is_comment (Token (_, (Comment, _))) = true
-  | is_comment (Token (_, (Comment_Cartouche, _))) = true
+fun is_comment (Token (_, (Comment _, _))) = true
   | is_comment _ = false;
 
 fun warn tok =
@@ -152,8 +150,7 @@
   | Real => (Markup.ML_numeral, "")
   | Char => (Markup.ML_char, "")
   | String => (if SML then Markup.SML_string else Markup.ML_string, "")
-  | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
-  | Comment_Cartouche => (if SML then Markup.SML_comment else Markup.ML_comment, "")
+  | Comment _ => (if SML then Markup.SML_comment else Markup.ML_comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
@@ -178,7 +175,6 @@
 open Basic_Symbol_Pos;
 
 val err_prefix = "SML lexical error: ";
-val err_prefix' = "Isabelle/ML lexical error: ";
 
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
@@ -299,8 +295,8 @@
  (scan_char >> token Char ||
   scan_string >> token String ||
   scan_blanks1 >> token Space ||
-  Symbol_Pos.scan_comment err_prefix >> token Comment ||
-  Symbol_Pos.scan_comment_cartouche err_prefix' >> token Comment_Cartouche ||
+  Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
+  Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) ||
   Scan.max token_leq
    (Scan.literal lexicon >> token Keyword)
    (scan_word >> token Word ||

--- a/src/Pure/ROOT.ML	Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/ROOT.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -44,6 +44,7 @@
 ML_file "General/position.ML";
 ML_file "General/symbol_pos.ML";
 ML_file "General/input.ML";
+ML_file "General/comment.ML";
 ML_file "General/antiquote.ML";
 ML_file "ML/ml_lex.ML";
 ML_file "ML/ml_compiler1.ML";

--- a/src/Pure/Syntax/lexicon.ML	Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -22,7 +22,7 @@
   val is_tid: string -> bool
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy |
-    StrSy | StringSy | Cartouche | Space | Cancel | Comment | Comment_Cartouche | EOF
+    StrSy | StringSy | Cartouche | Space | Comment of Comment.kind option | EOF
   datatype token = Token of token_kind * string * Position.range
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
@@ -114,7 +114,7 @@
 
 datatype token_kind =
   Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | StrSy |
-  StringSy | Cartouche | Space | Cancel | Comment | Comment_Cartouche | EOF;
+  StringSy | Cartouche | Space | Comment of Comment.kind option | EOF;
 
 datatype token = Token of token_kind * string * Position.range;
 
@@ -122,9 +122,7 @@
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;
 
-val is_proper =
-  kind_of_token #>
-  (fn Space => false | Cancel => false | Comment => false | Comment_Cartouche => false | _ => true);
+val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
 
 (* stopper *)
@@ -169,7 +167,7 @@
   | StrSy => Markup.inner_string
   | StringSy => Markup.inner_string
   | Cartouche => Markup.inner_cartouche
-  | Comment => Markup.inner_comment
+  | Comment NONE => Markup.inner_comment
   | _ => Markup.empty;
 
 fun report_of_token (Token (kind, s, (pos, _))) =
@@ -268,9 +266,8 @@
 
     val scan_token =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
-      Symbol_Pos.scan_cancel_cartouche Symbol.cancel >> token Cancel ||
-      Symbol_Pos.scan_comment err_prefix >> token Comment ||
-      Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment_Cartouche ||
+      Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
+      Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token StringSy ||
       scan_str >> token StrSy ||

--- a/src/Pure/Thy/thy_output.ML	Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -67,34 +67,7 @@
   end;
 
 
-(* output tokens with operators *)
-
-datatype operator = No_Operator | Cancel | Comment;
-
-local
-
-open Basic_Symbol_Pos;
-
-fun is_operator sym = sym = Symbol.cancel orelse sym = Symbol.comment;
-
-fun scan_operator blanks operator_symbol operator =
-  (if blanks then $$$ operator_symbol @@@ Symbol_Pos.scan_blanks else $$$ operator_symbol) --
-    Scan.option (Symbol_Pos.scan_cartouche "Document token error: ")
-      >> (fn (syms, NONE) => (No_Operator, syms) | (_, SOME syms) => (operator, syms));
-
-val scan_symbols_operator =
-  Scan.many1 (fn (s, _) => not (is_operator s) andalso Symbol.not_eof s) >> pair No_Operator ||
-  scan_operator false Symbol.cancel Cancel ||
-  scan_operator true Symbol.comment Comment;
-
-in
-
-fun read_symbols_operator syms =
-  if exists (is_operator o Symbol_Pos.symbol) syms then
-    Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_operator) syms
-  else NONE;
-
-end;
+(* output tokens with formal comments *)
 
 local
 
@@ -109,29 +82,29 @@
     | Antiquote.Antiq {body, ...} =>
         Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
 
-fun output_symbols_operator ctxt {antiq} (operator, syms) =
-  (case (operator, antiq) of
-    (No_Operator, false) => output_symbols syms
-  | (No_Operator, true) =>
+fun output_symbols_comment ctxt {antiq} (comment, syms) =
+  (case (comment, antiq) of
+    (NONE, false) => output_symbols syms
+  | (NONE, true) =>
       Antiquote.parse (#1 (Symbol_Pos.range syms)) syms
       |> maps output_symbols_antiq
-  | (Cancel, _) =>
-      output_symbols (Symbol_Pos.cartouche_content syms)
-      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
-  | (Comment, _) =>
+  | (SOME Comment.Comment, _) =>
       let
         val body = Symbol_Pos.cartouche_content syms;
         val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body);
       in
         output_text ctxt {markdown = false} source
         |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
-      end);
+      end
+  | (SOME Comment.Cancel, _) =>
+      output_symbols (Symbol_Pos.cartouche_content syms)
+      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}");
 
 in
 
 fun output_body ctxt antiq bg en syms =
-  (case read_symbols_operator syms of
-    SOME res => maps (output_symbols_operator ctxt {antiq = antiq}) res
+  (case Comment.read_body syms of
+    SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res
   | NONE => output_symbols syms) |> Latex.enclose_body bg en
 and output_token ctxt tok =
   let
@@ -153,19 +126,18 @@
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
 fun check_comments ctxt =
-  read_symbols_operator #> (Option.app o List.app) (fn (operator, syms) =>
+  Comment.read_body #> (Option.app o List.app) (fn (comment, syms) =>
     let
       val pos = #1 (Symbol_Pos.range syms);
       val markup =
-        (case operator of
-          No_Operator => NONE
-        | Cancel => SOME (Markup.language_text true)
-        | Comment => SOME (Markup.language_document true));
+        comment |> Option.map
+          (fn Comment.Comment => Markup.language_document true
+            | Comment.Cancel => Markup.language_text true);
       val _ =
         markup |> Option.app (fn m =>
           Context_Position.reports ctxt [(pos, m), (pos, Markup.cartouche)]);
-      val _ = output_symbols_operator ctxt {antiq = false} (operator, syms);
-    in if operator = Comment then check_comments ctxt syms else () end);
+      val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
+    in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
 
 fun check_token_comments ctxt tok =
   check_comments ctxt (Input.source_explode (Token.input_of tok));

--- a/src/Pure/Tools/rail.ML	Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/Tools/rail.ML	Sun Jan 14 14:11:02 2018 +0100
@@ -44,7 +44,7 @@
 (* datatype token *)
 
 datatype kind =
-  Keyword | Ident | String | Space | Comment | Antiq of Antiquote.antiq | EOF;
+  Keyword | Ident | String | Space | Comment of Comment.kind | Antiq of Antiquote.antiq | EOF;
 
 datatype token = Token of Position.range * (kind * string);
 
@@ -60,7 +60,7 @@
 fun content_of (Token (_, (_, x))) = x;
 
 fun is_proper (Token (_, (Space, _))) = false
-  | is_proper (Token (_, (Comment, _))) = false
+  | is_proper (Token (_, (Comment _, _))) = false
   | is_proper _ = true;
 
 
@@ -71,7 +71,7 @@
   | Ident => "identifier"
   | String => "single-quoted string"
   | Space => "white space"
-  | Comment => "formal comment"
+  | Comment _ => "formal comment"
   | Antiq _ => "antiquotation"
   | EOF => "end-of-input";
 
@@ -118,7 +118,7 @@
 
 val scan_token =
   scan_space >> token Space ||
-  Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment ||
+  Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)||
   Antiquote.scan_antiq >> antiq_token ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||