# HG changeset patch
# User wenzelm
# Date 1218364706 -7200
# Node ID a6319699e517c1de99c191349750656fe00fa566
# Parent  0ead8c2428f92d56a1f0c51d6dae0bfb6930b6ee
added parse_token (from proof_context.ML);

diff -r 0ead8c2428f9 -r a6319699e517 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,