Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML/ml_lex.ML
changeset 67425 7d4a088dbc0e
parent 67363 408a137e2793
child 67427 5409cfd41e7f 
--- 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 ||
isabelle