--- a/src/Pure/General/markup.ML Fri Mar 20 20:21:38 2009 +0100
+++ b/src/Pure/General/markup.ML Fri Mar 20 20:22:13 2009 +0100
@@ -62,6 +62,14 @@
val propN: string val prop: T
val attributeN: string val attribute: string -> T
val methodN: string val method: string -> T
+ val ML_keywordN: string val ML_keyword: T
+ val ML_identN: string val ML_ident: T
+ val ML_tvarN: string val ML_tvar: T
+ val ML_numeralN: string val ML_numeral: T
+ val ML_charN: string val ML_char: T
+ val ML_stringN: string val ML_string: T
+ val ML_commentN: string val ML_comment: T
+ val ML_malformedN: string val ML_malformed: T
val ML_sourceN: string val ML_source: T
val doc_sourceN: string val doc_source: T
val antiqN: string val antiq: T
@@ -213,6 +221,18 @@
val (methodN, method) = markup_string "method" nameN;
+(* ML syntax *)
+
+val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
+val (ML_identN, ML_ident) = markup_elem "ML_ident";
+val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
+val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
+val (ML_charN, ML_char) = markup_elem "ML_char";
+val (ML_stringN, ML_string) = markup_elem "ML_string";
+val (ML_commentN, ML_comment) = markup_elem "ML_comment";
+val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
+
+
(* embedded source text *)
val (ML_sourceN, ML_source) = markup_elem "ML_source";
--- a/src/Pure/ML/ml_context.ML Fri Mar 20 20:21:38 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Fri Mar 20 20:22:13 2009 +0100
@@ -194,7 +194,7 @@
fun eval_antiquotes (txt, pos) opt_context =
let
val syms = Symbol_Pos.explode (txt, pos);
- val ants = Antiquote.read ML_Lex.scan_antiq (syms, pos);
+ val ants = Antiquote.read ML_Lex.report_token ML_Lex.scan_antiq (syms, pos);
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
val ((ml_env, ml_body), opt_ctxt') =
if not (exists Antiquote.is_antiq ants)
--- a/src/Pure/ML/ml_lex.ML Fri Mar 20 20:21:38 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML Fri Mar 20 20:22:13 2009 +0100
@@ -16,6 +16,8 @@
val pos_of: token -> string
val kind_of: token -> token_kind
val content_of: token -> string
+ val markup_of: token -> Markup.T
+ val report_token: token -> unit
val keywords: string list
val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list
val source: (Symbol.symbol, 'a) Source.source ->
@@ -74,6 +76,26 @@
| is_improper _ = false;
+(* markup *)
+
+val markup_of = kind_of #>
+ (fn Keyword => Markup.ML_keyword
+ | Ident => Markup.ML_ident
+ | LongIdent => Markup.ML_ident
+ | 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.none
+ | Comment => Markup.ML_comment
+ | Error _ => Markup.ML_malformed
+ | EOF => Markup.none);
+
+fun report_token tok = Position.report (markup_of tok) (position_of tok);
+
+
(** scanners **)