src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Sun Aug 10 12:38:25 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Aug 10 12:38:26 2008 +0200
@@ -83,6 +83,7 @@
     (string * string) trrule list -> syntax -> syntax
   val update_trrules_i: ast trrule list -> syntax -> syntax
   val remove_trrules_i: ast trrule list -> syntax -> syntax
+  val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
   val parse_term: Proof.context -> string -> term
@@ -694,6 +695,12 @@
 
 (* (un)parsing *)
 
+fun parse_token markup str =
+  let
+    val (syms, pos) = read_token str;
+    val _ = Position.report markup pos;
+  in (syms, pos) end;
+
 local
   type operations =
    {parse_sort: Proof.context -> string -> sort,