report_token/parse_token: back to context-less version;

--- a/src/Pure/Syntax/lexicon.ML	Mon Sep 29 21:26:39 2008 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Sep 29 21:26:41 2008 +0200
@@ -56,7 +56,7 @@
   val tvarT: typ
   val terminals: string list
   val is_terminal: string -> bool
-  val report_token: Proof.context -> token -> unit
+  val report_token: token -> unit
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
   val predef_term: string -> token option
@@ -162,8 +162,8 @@
   | Comment     => Markup.inner_comment
   | EOF         => Markup.none;
 
-fun report_token ctxt (Token (kind, _, (pos, _))) =
-  ContextPosition.report ctxt (token_kind_markup kind) pos;
+fun report_token (Token (kind, _, (pos, _))) =
+  Position.report (token_kind_markup kind) pos;
 
 
 (* matching_tokens *)

--- a/src/Pure/Syntax/syntax.ML	Mon Sep 29 21:26:39 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 29 21:26:41 2008 +0200
@@ -83,7 +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: Proof.context -> Markup.T -> string -> SymbolPos.T list * Position.T
+  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
@@ -482,7 +482,7 @@
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val toks = Lexicon.tokenize lexicon xids syms;
-    val _ = List.app (Lexicon.report_token ctxt) toks;
+    val _ = List.app Lexicon.report_token toks;
 
     val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
     val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
@@ -695,10 +695,10 @@
 
 (* (un)parsing *)
 
-fun parse_token ctxt markup str =
+fun parse_token markup str =
   let
     val (syms, pos) = read_token str;
-    val _ = ContextPosition.report ctxt markup pos;
+    val _ = Position.report markup pos;
   in (syms, pos) end;
 
 local