src/Pure/Isar/token.ML

   datatype kind =
     (*immediate source*)
     Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
     Float | Space |
     (*delimited content*)
-    String | Alt_String | Verbatim | Cartouche | Comment |
+    String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
     (*special content*)
     Error of string | EOF
   val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   type T

   val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool
   val is_improper: T -> bool
   val is_comment: T -> bool
+  val is_informal_comment: T -> bool
+  val is_formal_comment: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
   val is_error: T -> bool
   val is_space: T -> bool
   val is_blank: T -> bool

 datatype kind =
   (*immediate source*)
   Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
   Float | Space |
   (*delimited content*)
-  String | Alt_String | Verbatim | Cartouche | Comment |
+  String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
   (*special content*)
   Error of string | EOF;
 
 val str_of_kind =
  fn Command => "command"

   | Space => "white space"
   | String => "quoted string"
   | Alt_String => "back-quoted string"
   | Verbatim => "verbatim text"
   | Cartouche => "text cartouche"
-  | Comment => "comment text"
+  | Comment NONE => "informal comment"
+  | Comment (SOME _) => "formal comment"
   | Error _ => "bad input"
   | EOF => "end-of-input";
 
 val immediate_kinds =
   Vector.fromList
     [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space];
 
-val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment];
+val delimited_kind =
+  (fn String => true
+    | Alt_String => true
+    | Verbatim => true
+    | Cartouche => true
+    | Comment _ => true
+    | _ => false);
 
 
 (* datatype token *)
 
 (*The value slot assigns an (optional) internal value to a token,

 
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;
 
 fun is_proper (Token (_, (Space, _), _)) = false
-  | is_proper (Token (_, (Comment, _), _)) = false
+  | is_proper (Token (_, (Comment _, _), _)) = false
   | is_proper _ = true;
 
 val is_improper = not o is_proper;
 
-fun is_comment (Token (_, (Comment, _), _)) = true
+fun is_comment (Token (_, (Comment _, _), _)) = true
   | is_comment _ = false;
 
-fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
+fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true
+  | is_informal_comment _ = false;
+
+fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
+  | is_formal_comment _ = false;
+
+fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
   | is_begin_ignore _ = false;
 
-fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
+fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true
   | is_end_ignore _ = false;
 
 fun is_error (Token (_, (Error _, _), _)) = true
   | is_error _ = false;
 

   | Type_Var => (Markup.tvar, "")
   | String => (Markup.string, "")
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
-  | Comment => (Markup.comment, "")
+  | Comment NONE => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
 

   (case kind of
     String => Symbol_Pos.quote_string_qq x
   | Alt_String => Symbol_Pos.quote_string_bq x
   | Verbatim => enclose "{*" "*}" x
   | Cartouche => cartouche x
-  | Comment => enclose "(*" "*)" x
+  | Comment NONE => enclose "(*" "*)" x
   | EOF => ""
   | _ => x);
 
 fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
 

 fun scan_token keywords = !!! "bad input"
   (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
     scan_verbatim >> token_range Verbatim ||
     scan_cartouche >> token_range Cartouche ||
-    scan_comment >> token_range Comment ||
+    scan_comment >> token_range (Comment NONE) ||
+    (Comment.scan_cancel || Comment.scan_latex) >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
     scan_space >> token Space ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
         (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))