# HG changeset patch
# User wenzelm
# Date 1460725723 -7200
# Node ID d2e3b3b159d7c2b6d2a35ffd397fc8f7bc5d59ad
# Parent  35f1475e9ced0f41c5893183dba67f55e2582ddf
clarified PIDE reports;

diff -r 35f1475e9ced -r d2e3b3b159d7 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Apr 15 14:27:59 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Apr 15 15:08:43 2016 +0200
@@ -327,7 +327,9 @@
     lthy
     |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
     |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
+    |> Context_Position.set_visible false
     |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
+    ||> Context_Position.restore_visible lthy
   end;
 
 
diff -r 35f1475e9ced -r d2e3b3b159d7 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Fri Apr 15 14:27:59 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Fri Apr 15 15:08:43 2016 +0200
@@ -90,7 +90,7 @@
   let
     val ((xs, mxs), specs) = defs |> split_list |>> split_list;
     val (bs, rhss) = specs |> split_list;
-    val eqs = mk_def ctxt (xs ~~ rhss);
+    val eqs = mk_def (Context_Position.set_visible false ctxt) (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
diff -r 35f1475e9ced -r d2e3b3b159d7 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Apr 15 14:27:59 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Apr 15 15:08:43 2016 +0200
@@ -740,7 +740,7 @@
       #-> (fn rhss =>
         let
           val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
-            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
+            ((x, mx), ((Binding.reset_pos (Thm.def_binding_optional x a), atts), rhs)));
         in map_context_result (Local_Defs.add_defs defs) end))
     |-> (set_facts o map (#2 o #2))
   end;
diff -r 35f1475e9ced -r d2e3b3b159d7 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Apr 15 14:27:59 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Apr 15 15:08:43 2016 +0200
@@ -130,7 +130,14 @@
 fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let
     val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
-    val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
+    val (xs, params_ctxt) = vars_ctxt
+      |> Context_Position.set_visible false
+      |> Proof_Context.add_fixes vars
+      ||> Context_Position.restore_visible vars_ctxt;
+    val _ =
+      Context_Position.reports params_ctxt
+        (map (Binding.pos_of o #1) vars ~~
+          map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
 
     val Asss =
       (map o map) snd raw_specss