ContextPosition.report;
parse_token/report_token: explicit context;

--- a/src/Pure/Isar/proof_context.ML	Mon Sep 29 14:41:24 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 29 14:41:25 2008 +0200
@@ -238,7 +238,7 @@
     (mode, naming, syntax, consts, facts, f cases));
 
 val get_mode = #mode o rep_context;
-fun restore_mode ctxt = set_mode (get_mode ctxt);
+val restore_mode = set_mode o get_mode;
 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
 
 fun set_stmt stmt =
@@ -443,7 +443,7 @@
     (case Variable.lookup_const ctxt c of
       SOME d => Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => error msg)
     | NONE => Consts.read_const (consts_of ctxt) c)
-  in Position.report (Markup.const d) pos; t end;
+  in ContextPosition.report ctxt (Markup.const d) pos; t end;
 
 in
 
@@ -453,12 +453,12 @@
     val (c, pos) = token_content str;
   in
     if Syntax.is_tid c then
-     (Position.report Markup.tfree pos;
+     (ContextPosition.report ctxt Markup.tfree pos;
       TFree (c, the_default (Sign.defaultS thy) (Variable.def_sort ctxt (c, ~1))))
     else
       let
         val d = Sign.intern_type thy c;
-        val _ = Position.report (Markup.tycon d) pos;
+        val _ = ContextPosition.report ctxt (Markup.tycon d) pos;
       in Type (d, replicate (Sign.arity_number thy d) dummyT) end
   end;
 
@@ -468,7 +468,7 @@
   let val (c, pos) = token_content str in
     (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
-        (Position.report (Markup.name x
+        (ContextPosition.report ctxt (Markup.name x
             (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
           Free (x, infer_type ctxt x))
     | _ => prep_const_proper ctxt (c, pos))
@@ -687,7 +687,7 @@
 
 fun parse_sort ctxt text =
   let
-    val (syms, pos) = Syntax.parse_token Markup.sort text;
+    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
         (Sign.intern_sort (theory_of ctxt)) (syms, pos)
       handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
@@ -698,7 +698,7 @@
     val thy = ProofContext.theory_of ctxt;
     val get_sort = get_sort thy (Variable.def_sort ctxt);
 
-    val (syms, pos) = Syntax.parse_token Markup.typ text;
+    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
     val T = Sign.intern_tycons thy
         (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
       handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
@@ -711,7 +711,7 @@
 
     val (T', _) = TypeInfer.paramify_dummies T 0;
     val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
-    val (syms, pos) = Syntax.parse_token markup text;
+    val (syms, pos) = Syntax.parse_token ctxt markup text;
 
     fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
       handle ERROR msg => SOME msg;
@@ -932,7 +932,7 @@
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
           else
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
-              SOME (_, ths) => (Position.report (Markup.local_fact name) pos;
+              SOME (_, ths) => (ContextPosition.report ctxt (Markup.local_fact name) pos;
                 map (Thm.transfer thy) (Facts.select thmref ths))
             | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;
@@ -971,7 +971,7 @@
     val bname = Name.name_of binding;
     val pos = Name.pos_of binding;
     val name = full_name ctxt bname;
-    val _ = Position.report (Markup.local_fact_decl name) pos;
+    val _ = ContextPosition.report ctxt (Markup.local_fact_decl name) pos;
 
     val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
     fun app (th, attrs) x =
@@ -1118,7 +1118,7 @@
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
     val _ = (vars ~~ xs') |> List.app (fn ((binding, _, _), x') =>
-      Position.report (Markup.fixed_decl x') (Name.pos_of binding));
+      ContextPosition.report ctxt (Markup.fixed_decl x') (Name.pos_of binding));
   in (xs', ctxt'') end;
 
 in

--- a/src/Pure/ML/ml_context.ML	Mon Sep 29 14:41:24 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Sep 29 14:41:25 2008 +0200
@@ -173,7 +173,7 @@
   let val ((name, _), pos) = Args.dest_src src in
     (case Symtab.lookup (! global_parsers) name of
       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | SOME scan => (Position.report (Markup.ML_antiq name) pos;
+    | SOME scan => (ContextPosition.report ctxt (Markup.ML_antiq name) pos;
         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   end;
 

--- a/src/Pure/Syntax/lexicon.ML	Mon Sep 29 14:41:24 2008 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Sep 29 14:41:25 2008 +0200
@@ -56,7 +56,7 @@
   val tvarT: typ
   val terminals: string list
   val is_terminal: string -> bool
-  val report_token: token -> unit
+  val report_token: Proof.context -> 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 (Token (kind, _, (pos, _))) =
-  Position.report (token_kind_markup kind) pos;
+fun report_token ctxt (Token (kind, _, (pos, _))) =
+  ContextPosition.report ctxt (token_kind_markup kind) pos;
 
 
 (* matching_tokens *)

--- a/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:41:24 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:41:25 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: Markup.T -> string -> SymbolPos.T list * Position.T
+  val parse_token: Proof.context -> 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 toks;
+    val _ = List.app (Lexicon.report_token ctxt) 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 markup str =
+fun parse_token ctxt markup str =
   let
     val (syms, pos) = read_token str;
-    val _ = Position.report markup pos;
+    val _ = ContextPosition.report ctxt markup pos;
   in (syms, pos) end;
 
 local