--- a/src/Pure/ML/ml_lex.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/ML/ml_lex.ML Sun Nov 25 19:49:24 2012 +0100
@@ -104,23 +104,23 @@
local
val token_kind_markup =
- fn Keyword => (Isabelle_Markup.ML_keyword, "")
+ fn Keyword => (Markup.ML_keyword, "")
| Ident => (Markup.empty, "")
| LongIdent => (Markup.empty, "")
- | TypeVar => (Isabelle_Markup.ML_tvar, "")
- | Word => (Isabelle_Markup.ML_numeral, "")
- | Int => (Isabelle_Markup.ML_numeral, "")
- | Real => (Isabelle_Markup.ML_numeral, "")
- | Char => (Isabelle_Markup.ML_char, "")
- | String => (Isabelle_Markup.ML_string, "")
+ | TypeVar => (Markup.ML_tvar, "")
+ | Word => (Markup.ML_numeral, "")
+ | Int => (Markup.ML_numeral, "")
+ | Real => (Markup.ML_numeral, "")
+ | Char => (Markup.ML_char, "")
+ | String => (Markup.ML_string, "")
| Space => (Markup.empty, "")
- | Comment => (Isabelle_Markup.ML_comment, "")
- | Error msg => (Isabelle_Markup.bad, msg)
+ | Comment => (Markup.ML_comment, "")
+ | Error msg => (Markup.bad, msg)
| EOF => (Markup.empty, "");
fun token_markup kind x =
if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
- then (Isabelle_Markup.ML_delimiter, "")
+ then (Markup.ML_delimiter, "")
else token_kind_markup kind;
in
@@ -289,7 +289,7 @@
fun read pos txt =
let
- val _ = Position.report pos Isabelle_Markup.ML_source;
+ val _ = Position.report pos Markup.ML_source;
val syms = Symbol_Pos.explode (txt, pos);
val termination =
if null syms then []