prefer Context_Position.report where a proper context is available -- notably for "inner" entities;

--- a/src/Pure/Isar/proof_context.ML	Sun Aug 08 19:36:31 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Aug 08 19:54:54 2010 +0200
@@ -334,7 +334,7 @@
     val (syms, pos) = Syntax.read_token text;
     val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
       handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
-    val _ = Position.report (Markup.tclass c) pos;
+    val _ = Context_Position.report ctxt (Markup.tclass c) pos;
   in c end;
 
 
@@ -469,7 +469,7 @@
     val _ =
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();
-    val _ = Position.report (Markup.const d) pos;
+    val _ = Context_Position.report ctxt (Markup.const d) pos;
   in t end;
 
 in
@@ -480,13 +480,13 @@
     val (c, pos) = token_content text;
   in
     if Syntax.is_tid c then
-     (Position.report Markup.tfree pos;
+     (Context_Position.report ctxt Markup.tfree pos;
       TFree (c, default_sort ctxt (c, ~1)))
     else
       let
         val d = Type.intern_type tsig c;
         val decl = Type.the_decl tsig d;
-        val _ = Position.report (Markup.tycon d) pos;
+        val _ = Context_Position.report ctxt (Markup.tycon d) pos;
         fun err () = error ("Bad type name: " ^ quote d);
         val args =
           (case decl of
@@ -511,7 +511,7 @@
   in
     (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
-        (Position.report (Markup.name x
+        (Context_Position.report ctxt (Markup.name x
             (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
           Free (x, infer_type ctxt (x, ty)))
     | _ => prep_const_proper ctxt strict (c, pos))
@@ -977,7 +977,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) => (Context_Position.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;
@@ -1007,7 +1007,7 @@
   let
     val pos = Binding.pos_of b;
     val name = full_name ctxt b;
-    val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
+    val _ = Context_Position.report ctxt (Markup.local_fact_decl name) pos;
 
     val facts = PureThy.name_thmss false name raw_facts;
     fun app (th, attrs) x =
@@ -1186,7 +1186,7 @@
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
     val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
+      Context_Position.report ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   in (xs', ctxt'') end;
 
 

--- a/src/Pure/ML/ml_context.ML	Sun Aug 08 19:36:31 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Sun Aug 08 19:54:54 2010 +0200
@@ -105,7 +105,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 => (Context_Position.report ctxt (Markup.ML_antiq name) pos;
         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   end;
 

--- a/src/Pure/Syntax/lexicon.ML	Sun Aug 08 19:36:31 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sun Aug 08 19:54:54 2010 +0200
@@ -65,7 +65,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
@@ -185,8 +185,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, _))) =
+  Context_Position.report ctxt (token_kind_markup kind) pos;
 
 
 (* matching_tokens *)

--- a/src/Pure/Syntax/syntax.ML	Sun Aug 08 19:36:31 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Aug 08 19:54:54 2010 +0200
@@ -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 Syn_Ext.logic else root;
     val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);

--- a/src/Pure/context_position.ML	Sun Aug 08 19:36:31 2010 +0200
+++ b/src/Pure/context_position.ML	Sun Aug 08 19:54:54 2010 +0200
@@ -9,7 +9,7 @@
   val is_visible: Proof.context -> bool
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
-  val report_visible: Proof.context -> Markup.T -> Position.T -> unit
+  val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
 
 structure Context_Position: CONTEXT_POSITION =
@@ -25,7 +25,7 @@
 val set_visible = Data.put;
 val restore_visible = set_visible o is_visible;
 
-fun report_visible ctxt markup pos =
+fun report ctxt markup pos =
   if is_visible ctxt then Position.report markup pos else ();
 
 end;