--- a/src/Doc/antiquote_setup.ML Wed Dec 03 11:37:51 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Wed Dec 03 11:50:58 2014 +0100
@@ -62,7 +62,8 @@
ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
| ml_functor _ = raise Fail "Bad ML functor specification";
-val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);
+val is_name =
+ ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
fun ml_name txt =
(case filter is_name (ML_Lex.tokenize txt) of
--- a/src/Pure/ML/ml_lex.ML Wed Dec 03 11:37:51 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Wed Dec 03 11:50:58 2014 +0100
@@ -8,7 +8,7 @@
sig
val keywords: string list
datatype token_kind =
- Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
+ Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
Space | Comment | Error of string | EOF
eqtype token
val stopper: token Scan.stopper
@@ -61,7 +61,7 @@
(* datatype token *)
datatype token_kind =
- Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
+ Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
Space | Comment | Error of string | EOF;
datatype token = Token of Position.range * (token_kind * string);
@@ -135,19 +135,19 @@
local
fun token_kind_markup SML =
- fn Keyword => (Markup.empty, "")
- | Ident => (Markup.empty, "")
- | LongIdent => (Markup.empty, "")
- | TypeVar => (Markup.ML_tvar, "")
- | Word => (Markup.ML_numeral, "")
- | Int => (Markup.ML_numeral, "")
- | Real => (Markup.ML_numeral, "")
- | Char => (Markup.ML_char, "")
- | String => (if SML then Markup.SML_string else Markup.ML_string, "")
- | Space => (Markup.empty, "")
- | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
+ fn Keyword => (Markup.empty, "")
+ | Ident => (Markup.empty, "")
+ | Long_Ident => (Markup.empty, "")
+ | Type_Var => (Markup.ML_tvar, "")
+ | Word => (Markup.ML_numeral, "")
+ | Int => (Markup.ML_numeral, "")
+ | Real => (Markup.ML_numeral, "")
+ | Char => (Markup.ML_char, "")
+ | String => (if SML then Markup.SML_string else Markup.ML_string, "")
+ | Space => (Markup.empty, "")
+ | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
| Error msg => (Markup.bad, msg)
- | EOF => (Markup.empty, "");
+ | EOF => (Markup.empty, "");
in
@@ -280,9 +280,9 @@
(scan_word >> token Word ||
scan_real >> token Real ||
scan_int >> token Int ||
- scan_long_ident >> token LongIdent ||
+ scan_long_ident >> token Long_Ident ||
scan_ident >> token Ident ||
- scan_type_var >> token TypeVar));
+ scan_type_var >> token Type_Var));
val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;