more markup for inner syntax class/type names (notably for completion);
explicit reports result without broadcast yet, which is important for brute-force disambiguation;

--- a/src/Pure/General/name_space.ML	Wed Mar 05 17:36:40 2014 +0100
+++ b/src/Pure/General/name_space.ML	Wed Mar 05 18:26:35 2014 +0100
@@ -55,6 +55,8 @@
   val map_naming: (naming -> naming) -> Context.generic -> Context.generic
   val declare: Context.generic -> bool -> binding -> T -> string * T
   type 'a table = T * 'a Symtab.table
+  val check_reports: Context.generic -> 'a table ->
+    xstring * Position.T -> (string * Position.report list) * 'a
   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
   val get: 'a table -> string -> 'a
   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
@@ -445,18 +447,27 @@
 
 type 'a table = T * 'a Symtab.table;
 
-fun check context (space, tab) (xname, pos) =
+fun check_reports context (space, tab) (xname, pos) =
   let val name = intern space xname in
     (case Symtab.lookup tab name of
       SOME x =>
-       (Context_Position.report_generic context pos (markup space name);
-        (name, x))
+        let
+          val reports =
+            if Context_Position.is_visible_generic context andalso Position.is_reported pos
+            then [(pos, markup space name)] else [];
+        in ((name, reports), x) end
     | NONE =>
         error (undefined (kind_of space) name ^ Position.here pos ^
           Markup.markup Markup.report
             (Completion.reported_text (completion context space (xname, pos)))))
   end;
 
+fun check context table arg =
+  let
+    val ((name, reports), x) = check_reports context table arg;
+    val _ = Position.reports reports;
+  in (name, x) end;
+
 fun get (space, tab) name =
   (case Symtab.lookup tab name of
     SOME x => x

--- a/src/Pure/General/position.ML	Wed Mar 05 17:36:40 2014 +0100
+++ b/src/Pure/General/position.ML	Wed Mar 05 18:26:35 2014 +0100
@@ -41,7 +41,8 @@
   type report_text = report * string
   val reports_text: report_text list -> unit
   val reports: report list -> unit
-  val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
+  val store_reports: report_text list Unsynchronized.ref ->
+    T list -> ('a -> Markup.T list) -> 'a -> unit
   val here: T -> string
   val here_list: T list -> string
   type range = T * T
@@ -177,9 +178,9 @@
 val reports = map (rpair "") #> reports_text;
 
 fun store_reports _ [] _ _ = ()
-  | store_reports (r: report list Unsynchronized.ref) ps markup x =
+  | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
       let val ms = markup x
-      in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
+      in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
 
 
 (* here: inlined formal markup *)

--- a/src/Pure/Isar/proof_context.ML	Wed Mar 05 17:36:40 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 05 18:26:35 2014 +0100
@@ -57,7 +57,8 @@
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val markup_fact: Proof.context -> string -> Markup.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
-  val read_class: Proof.context -> xstring -> class
+  val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
+  val read_class: Proof.context -> string -> class
   val read_typ: Proof.context -> string -> typ
   val read_typ_syntax: Proof.context -> string -> typ
   val read_typ_abbrev: Proof.context -> string -> typ
@@ -67,6 +68,10 @@
   val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
+  val check_type_name: Proof.context -> bool ->
+    xstring * Position.T -> typ * Position.report list
+  val check_type_name_proper: Proof.context -> bool ->
+    xstring * Position.T -> typ * Position.report list
   val read_type_name: Proof.context -> bool -> string -> typ
   val read_type_name_proper: Proof.context -> bool -> string -> typ
   val read_const_proper: Proof.context -> bool -> string -> term
@@ -374,20 +379,27 @@
 
 (* classes *)
 
-fun read_class ctxt text =
+fun check_class ctxt (xname, pos) =
   let
     val tsig = tsig_of ctxt;
     val class_space = Type.class_space tsig;
 
-    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
     val name = Type.cert_class tsig (Type.intern_class tsig xname)
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
           Markup.markup Markup.report
             (Completion.reported_text
               (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
-    val _ = Context_Position.report ctxt pos (Name_Space.markup class_space name);
-  in name end;
+    val reports =
+      if Context_Position.is_visible ctxt andalso Position.is_reported pos
+      then [(pos, Name_Space.markup class_space name)] else [];
+  in (name, reports) end;
+
+fun read_class ctxt text =
+  let
+    val (c, reports) = check_class ctxt (Symbol_Pos.source_content (Syntax.read_token text));
+    val _ = Position.reports reports;
+  in c end;
 
 
 (* types *)
@@ -443,30 +455,34 @@
 
 (* type names *)
 
-fun read_type_name ctxt strict text =
-  let
-    val tsig = tsig_of ctxt;
-    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
-  in
-    if Lexicon.is_tid c then
-     (Context_Position.report ctxt pos Markup.tfree;
-      TFree (c, default_sort ctxt (c, ~1)))
-    else
-      let
-        val (d, decl) = Type.check_decl (Context.Proof ctxt) tsig (c, pos);
-        fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
-        val args =
-          (case decl of
-            Type.LogicalType n => n
-          | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
-          | Type.Nonterminal => if strict then err () else 0);
-      in Type (d, replicate args dummyT) end
-  end;
+fun check_type_name ctxt strict (c, pos) =
+  if Lexicon.is_tid c then
+    let
+      val reports =
+        if Context_Position.is_visible ctxt andalso Position.is_reported pos
+        then [(pos, Markup.tfree)] else [];
+    in (TFree (c, default_sort ctxt (c, ~1)), reports) end
+  else
+    let
+      val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
+      fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
+      val args =
+        (case decl of
+          Type.LogicalType n => n
+        | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
+        | Type.Nonterminal => if strict then err () else 0);
+    in (Type (d, replicate args dummyT), reports) end;
 
-fun read_type_name_proper ctxt strict text =
-  (case read_type_name ctxt strict text of
-    T as Type _ => T
-  | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
+fun check_type_name_proper ctxt strict arg =
+  (case check_type_name ctxt strict arg of
+    res as (Type _, _) => res
+  | (T, _) => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
+
+fun read_type_name ctxt strict =
+  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name ctxt strict #> #1;
+
+fun read_type_name_proper ctxt strict =
+  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name_proper ctxt strict #> #1;
 
 
 (* constant names *)

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Mar 05 17:36:40 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Mar 05 18:26:35 2014 +0100
@@ -10,7 +10,7 @@
   val decode_sort: term -> sort
   val decode_typ: term -> typ
   val decode_term: Proof.context ->
-    Position.report list * term Exn.result -> Position.report list * term Exn.result
+    Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
   val print_checks: Proof.context -> unit
@@ -138,7 +138,7 @@
 
 fun parsetree_to_ast ctxt trf parsetree =
   let
-    val reports = Unsynchronized.ref ([]: Position.report list);
+    val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report pos = Position.store_reports reports [pos];
 
     fun trans a args =
@@ -163,17 +163,15 @@
     and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
           let
             val pos = Lexicon.pos_of_token tok;
-            val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
-              handle ERROR msg => error (msg ^ Position.here pos);
-            val _ = report pos (markup_class ctxt) c;
+            val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
+            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
           in [Ast.Constant (Lexicon.mark_class c)] end
       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
           let
             val pos = Lexicon.pos_of_token tok;
-            val Type (c, _) =
-              Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok)
-                handle ERROR msg => error (msg ^ Position.here pos);
-            val _ = report pos (markup_type ctxt) c;
+            val (Type (c, _), rs) =
+              Proof_Context.check_type_name_proper ctxt false (Lexicon.str_of_token tok, pos);
+            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
@@ -222,7 +220,7 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
+fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
         fun get_const a =
@@ -286,8 +284,8 @@
 
 fun report_result ctxt pos ambig_msgs results =
   (case (proper_results results, failed_results results) of
-    ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
-  | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
+    ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; reraise exn)
+  | ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x)
   | _ =>
       if null ambig_msgs then
         error ("Parse error: ambiguous syntax" ^ Position.here pos)
@@ -421,7 +419,7 @@
   let
     val syn = Proof_Context.syn_of ctxt;
 
-    val reports = Unsynchronized.ref ([]: Position.report list);
+    val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report ps = Position.store_reports reports ps;
 
     fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c);
@@ -446,7 +444,7 @@
       parse_asts ctxt true root (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode [];
-    val _ = Context_Position.reports ctxt (! reports);
+    val _ = Context_Position.reports_text ctxt (! reports);
   in ast end;
 
 

--- a/src/Pure/type.ML	Wed Mar 05 17:36:40 2014 +0100
+++ b/src/Pure/type.ML	Wed Mar 05 18:26:35 2014 +0100
@@ -52,7 +52,8 @@
   val intern_type: tsig -> xstring -> string
   val extern_type: Proof.context -> tsig -> string -> xstring
   val is_logtype: tsig -> string -> bool
-  val check_decl: Context.generic -> tsig -> xstring * Position.T -> string * decl
+  val check_decl: Context.generic -> tsig ->
+    xstring * Position.T -> (string * Position.report list) * decl
   val the_decl: tsig -> string * Position.T -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
@@ -258,7 +259,7 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
-fun check_decl context (TSig {types, ...}) = Name_Space.check context types;
+fun check_decl context (TSig {types, ...}) = Name_Space.check_reports context types;
 
 fun the_decl tsig (c, pos) =
   (case lookup_type tsig c of