# HG changeset patch
# User wenzelm
# Date 1237576933 -3600
# Node ID 845bcfd3e9cd75bf38720c6ea80c99b7157672cc
# Parent  b22d35d9ef284696bdccf10889134f3e08d16e08
report markup for ML tokens;

diff -r b22d35d9ef28 -r 845bcfd3e9cd src/Pure/General/markup.ML
--- 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";
diff -r b22d35d9ef28 -r 845bcfd3e9cd src/Pure/ML/ml_context.ML
--- 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)
diff -r b22d35d9ef28 -r 845bcfd3e9cd src/Pure/ML/ml_lex.ML
--- 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 **)