# HG changeset patch
# User wenzelm
# Date 1417603858 -3600
# Node ID 25501ba956acb8af38f2d556cb812a5d99e741d0
# Parent  2ceb05ee0331232f4a7f7171d391dfbf24152d7b
tuned;

diff -r 2ceb05ee0331 -r 25501ba956ac src/Doc/antiquote_setup.ML
--- 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
diff -r 2ceb05ee0331 -r 25501ba956ac src/Pure/ML/ml_lex.ML
--- 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;