more accurate context position reports;

--- a/src/Pure/General/name_space.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/General/name_space.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -575,7 +575,7 @@
 fun check context table (xname, pos) =
   let
     val ((name, reports), x) = check_reports context table (xname, [pos]);
-    val _ = Position.reports reports;
+    val _ = Context_Position.reports_generic context reports;
   in (name, x) end;
 
 fun defined (Table (_, tab)) name = Change_Table.defined tab name;

--- a/src/Pure/Isar/proof_context.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -475,7 +475,7 @@
   let
     val source = Syntax.read_input text;
     val (c, reports) = check_class ctxt (Input.source_content source);
-    val _ = Position.reports reports;
+    val _ = Context_Position.reports ctxt reports;
   in c end;
 
 
@@ -536,11 +536,11 @@
         | Type.Nonterminal => if strict then err () else 0);
     in (Type (d, replicate args dummyT), reports) end;
 
-fun read_type_name ctxt flags text =
+fun read_type_name flags ctxt text =
   let
     val source = Syntax.read_input text;
-    val (T, reports) = check_type_name ctxt flags (Input.source_content source);
-    val _ = Position.reports reports;
+    val (T, reports) = check_type_name flags ctxt (Input.source_content source);
+    val _ = Context_Position.reports ctxt reports;
   in T end;
 
 
@@ -583,12 +583,12 @@
       | _ => ());
   in (t, reports) end;
 
-fun read_const ctxt flags text =
+fun read_const flags ctxt text =
   let
     val source = Syntax.read_input text;
     val (c, pos) = Input.source_content source;
-    val (t, reports) = check_const ctxt flags (c, [pos]);
-    val _ = Position.reports reports;
+    val (t, reports) = check_const flags ctxt (c, [pos]);
+    val _ = Context_Position.reports ctxt reports;
   in t end;
 
 

--- a/src/Pure/Isar/specification.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -323,7 +323,7 @@
 fun gen_alias decl check (b, arg) lthy =
   let
     val (c, reports) = check {proper = true, strict = false} lthy arg;
-    val _ = Position.reports reports;
+    val _ = Context_Position.reports lthy reports;
   in decl b c lthy end;
 
 val alias =

--- a/src/Pure/PIDE/document.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -603,7 +603,8 @@
 
     val parents =
       if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
-    val _ = Position.reports (map #2 parents_reports);
+    val _ = List.app (fn (thy, r) => Context_Position.reports_global thy [r]) parents_reports;
+
     val thy = Resources.begin_theory master_dir header parents;
     val _ = Output.status [Markup.markup_only Markup.initialized];
   in thy end;

--- a/src/Pure/Thy/thy_info.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -352,7 +352,9 @@
     val dir = Path.dir thy_path;
     val header = Thy_Header.make (name, pos) imports keywords;
 
-    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
+    val _ =
+      (imports ~~ parents) |> List.app (fn ((_, pos), thy) =>
+        Context_Position.reports_global thy [(pos, Theory.get_markup thy)]);
 
     val exec_id = Document_ID.make ();
     val _ =

--- a/src/Pure/Tools/rail.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/Tools/rail.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -309,7 +309,7 @@
     val toks = tokenize (Input.source_explode source);
     val _ = Context_Position.reports ctxt (maps reports_of_token toks);
     val rules = parse_rules (filter is_proper toks);
-    val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);
+    val _ = Context_Position.reports ctxt (maps (reports_of_tree ctxt o #2) rules);
   in map (apsnd prepare_tree) rules end;
 
 

--- a/src/Pure/context_position.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/context_position.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -19,17 +19,22 @@
   val restore_visible_global: theory -> theory -> theory
   val is_reported_generic: Context.generic -> Position.T -> bool
   val is_reported: Proof.context -> Position.T -> bool
+  val is_reported_global: theory -> Position.T -> bool
   val report_generic: Context.generic -> Position.T -> Markup.T -> unit
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   val report: Proof.context -> Position.T -> Markup.T -> unit
   val reports_text: Proof.context -> Position.report_text list -> unit
+  val reports_generic: Context.generic -> Position.report list -> unit
   val reports: Proof.context -> Position.report list -> unit
+  val reports_global: theory -> Position.report list -> unit
 end;
 
 structure Context_Position: CONTEXT_POSITION =
 struct
 
+(* visible context *)
+
 structure Data = Generic_Data
 (
   type T = bool option * bool option;  (*really, visible*)
@@ -54,8 +59,13 @@
 val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof;
 val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory;
 
+
+(* PIDE reports *)
+
 fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos;
-fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos;
+
+val is_reported = is_reported_generic o Context.Proof;
+val is_reported_global = is_reported_generic o Context.Theory;
 
 fun report_generic context pos markup =
   if is_reported_generic context pos then
@@ -69,6 +79,9 @@
 fun report ctxt pos markup = report_text ctxt pos markup "";
 
 fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else ();
-fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
+fun reports_generic context reps = if is_visible_generic context then Position.reports reps else ();
+
+val reports = reports_generic o Context.Proof;
+val reports_global = reports_generic o Context.Theory;
 
 end;

--- a/src/Pure/theory.ML	Fri Apr 03 12:45:14 2020 +0200
+++ b/src/Pure/theory.ML	Fri Apr 03 13:51:56 2020 +0200
@@ -130,7 +130,7 @@
 fun init_markup (name, pos) thy =
   let
     val id = serial ();
-    val _ = Position.report pos (theory_markup true name id pos);
+    val _ = Context_Position.reports_global thy [(pos, theory_markup true name id pos)];
   in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
 
 fun get_markup thy =