report proper binding positions only -- avoid swamping document model with unspecific information;

--- a/src/Pure/General/name_space.ML	Sat Sep 22 19:23:04 2012 +0200
+++ b/src/Pure/General/name_space.ML	Sat Sep 22 19:32:30 2012 +0200
@@ -400,7 +400,7 @@
     val name = Long_Name.implode (map fst spec);
     val _ = name = "" andalso err_bad binding;
 
-    val pos = Position.default (Binding.pos_of binding);
+    val (proper_pos, pos) = Position.default (Binding.pos_of binding);
     val entry =
      {concealed = concealed,
       group = group,
@@ -411,8 +411,10 @@
       |> fold (add_name name) accs
       |> new_entry strict (name, (accs', entry));
     val _ =
-      Context_Position.report_generic context pos
-        (entry_markup true (kind_of space) (name, entry));
+      if proper_pos then
+        Context_Position.report_generic context pos
+          (entry_markup true (kind_of space) (name, entry))
+      else ();
   in (name, space') end;
 
 

--- a/src/Pure/General/position.ML	Sat Sep 22 19:23:04 2012 +0200
+++ b/src/Pure/General/position.ML	Sat Sep 22 19:32:30 2012 +0200
@@ -49,7 +49,7 @@
   val range: T -> T -> range
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
-  val default: T -> T
+  val default: T -> bool * T
 end;
 
 structure Position: POSITION =
@@ -222,7 +222,7 @@
 end;
 
 fun default pos =
-  if pos = none then thread_data ()
-  else pos;
+  if pos = none then (false, thread_data ())
+  else (true, pos);
 
 end;