1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 06 14:38:54 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 06 16:12:26 2014 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    val declare: Context.generic -> bool -> binding -> T -> string * T
     1.5    type 'a table = T * 'a Symtab.table
     1.6    val check_reports: Context.generic -> 'a table ->
     1.7 -    xstring * Position.T -> (string * Position.report list) * 'a
     1.8 +    xstring * Position.T list -> (string * Position.report list) * 'a
     1.9    val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    1.10    val get: 'a table -> string -> 'a
    1.11    val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
    1.12 @@ -446,24 +446,27 @@
    1.13  
    1.14  type 'a table = T * 'a Symtab.table;
    1.15  
    1.16 -fun check_reports context (space, tab) (xname, pos) =
    1.17 +fun check_reports context (space, tab) (xname, ps) =
    1.18    let val name = intern space xname in
    1.19      (case Symtab.lookup tab name of
    1.20        SOME x =>
    1.21          let
    1.22            val reports =
    1.23 -            if Context_Position.is_reported_generic context pos
    1.24 -            then [(pos, markup space name)] else [];
    1.25 +            filter (Context_Position.is_reported_generic context) ps
    1.26 +            |> map (fn pos => (pos, markup space name));
    1.27          in ((name, reports), x) end
    1.28      | NONE =>
    1.29 -        error (undefined (kind_of space) name ^ Position.here pos ^
    1.30 -          Markup.markup Markup.report
    1.31 -            (Completion.reported_text (completion context space (xname, pos)))))
    1.32 +        let
    1.33 +          val completions = map (fn pos => completion context space (xname, pos)) ps;
    1.34 +        in
    1.35 +          error (undefined (kind_of space) name ^ Position.here_list ps ^
    1.36 +            implode (map (Markup.markup_report o Completion.reported_text) completions))
    1.37 +        end)
    1.38    end;
    1.39  
    1.40 -fun check context table arg =
    1.41 +fun check context table (xname, pos) =
    1.42    let
    1.43 -    val ((name, reports), x) = check_reports context table arg;
    1.44 +    val ((name, reports), x) = check_reports context table (xname, [pos]);
    1.45      val _ = Position.reports reports;
    1.46    in (name, x) end;
    1.47  

     2.1 --- a/src/Pure/Isar/args.ML	Thu Mar 06 14:38:54 2014 +0100
     2.2 +++ b/src/Pure/Isar/args.ML	Thu Mar 06 16:12:26 2014 +0100
     2.3 @@ -299,7 +299,7 @@
     2.4      | (_, (_, args2)) =>
     2.5          error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
     2.6            (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
     2.7 -          Markup.markup Markup.report (reported_text ())))
     2.8 +          Markup.markup_report (reported_text ())))
     2.9    end;
    2.10  
    2.11  fun context_syntax kind scan src =

     3.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 14:38:54 2014 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 16:12:26 2014 +0100
     3.3 @@ -71,6 +71,7 @@
     3.4    val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     3.5      xstring * Position.T -> typ * Position.report list
     3.6    val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
     3.7 +  val consts_completion_message: Proof.context -> xstring * Position.T list -> string
     3.8    val check_const: Proof.context -> {proper: bool, strict: bool} ->
     3.9      xstring * Position.T -> term * Position.report list
    3.10    val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
    3.11 @@ -384,9 +385,8 @@
    3.12      val name = Type.cert_class tsig (Type.intern_class tsig xname)
    3.13        handle TYPE (msg, _, _) =>
    3.14          error (msg ^ Position.here pos ^
    3.15 -          Markup.markup Markup.report
    3.16 -            (Completion.reported_text
    3.17 -              (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
    3.18 +          Markup.markup_report (Completion.reported_text
    3.19 +            (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
    3.20      val reports =
    3.21        if Context_Position.is_reported ctxt pos
    3.22        then [(pos, Name_Space.markup class_space name)] else [];
    3.23 @@ -469,8 +469,18 @@
    3.24  
    3.25  (* constant names *)
    3.26  
    3.27 +fun consts_completion_message ctxt (c, ps) =
    3.28 +  ps |> map (fn pos =>
    3.29 +    Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
    3.30 +    |> Completion.reported_text)
    3.31 +  |> implode
    3.32 +  |> Markup.markup_report;
    3.33 +
    3.34  fun check_const ctxt {proper, strict} (c, pos) =
    3.35    let
    3.36 +    val _ =
    3.37 +      Name.reject_internal (c, [pos]) handle ERROR msg =>
    3.38 +        error (msg ^ consts_completion_message ctxt (c, [pos]));
    3.39      fun err msg = error (msg ^ Position.here pos);
    3.40      val consts = consts_of ctxt;
    3.41      val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
    3.42 @@ -478,7 +488,6 @@
    3.43        (case (fixed, Variable.lookup_const ctxt c) of
    3.44          (SOME x, NONE) =>
    3.45            let
    3.46 -            val _ = Name.reject_internal (c, [pos]);
    3.47              val reports =
    3.48                if Context_Position.is_reported ctxt pos then
    3.49                  [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
    3.50 @@ -491,7 +500,7 @@
    3.51                if Context_Position.is_reported ctxt pos
    3.52                then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
    3.53            in (Const (d, T), reports) end
    3.54 -      | _ => Consts.check_const (Context.Proof ctxt) consts (c, pos));
    3.55 +      | _ => Consts.check_const (Context.Proof ctxt) consts (c, [pos]));
    3.56      val _ =
    3.57        (case (strict, t) of
    3.58          (true, Const (d, _)) =>

     4.1 --- a/src/Pure/PIDE/markup.ML	Thu Mar 06 14:38:54 2014 +0100
     4.2 +++ b/src/Pure/PIDE/markup.ML	Thu Mar 06 16:12:26 2014 +0100
     4.3 @@ -189,6 +189,7 @@
     4.4    val enclose: T -> Output.output -> Output.output
     4.5    val markup: T -> string -> string
     4.6    val markup_only: T -> string
     4.7 +  val markup_report: string -> string
     4.8  end;
     4.9  
    4.10  structure Markup: MARKUP =
    4.11 @@ -602,4 +603,7 @@
    4.12  
    4.13  fun markup_only m = markup m "";
    4.14  
    4.15 +fun markup_report "" = ""
    4.16 +  | markup_report txt = markup report txt;
    4.17 +
    4.18  end;

     5.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 14:38:54 2014 +0100
     5.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 16:12:26 2014 +0100
     5.3 @@ -274,14 +274,15 @@
     5.4                      val _ = report ps (markup_const ctxt) c;
     5.5                    in Const (c, T) end)
     5.6            | decode ps _ _ (Free (a, T)) =
     5.7 -              (Name.reject_internal (a, ps);
     5.8 -               case (get_free a, get_const a) of
     5.9 -                (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
    5.10 -              | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
    5.11 -              | (_, (false, c)) =>
    5.12 -                  if Long_Name.is_qualified c
    5.13 -                  then (report ps (markup_const ctxt) c; Const (c, T))
    5.14 -                  else (report ps (markup_free ctxt) c; Free (c, T)))
    5.15 +              ((Name.reject_internal (a, ps) handle ERROR msg =>
    5.16 +                  error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
    5.17 +                (case (get_free a, get_const a) of
    5.18 +                  (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
    5.19 +                | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
    5.20 +                | (_, (false, c)) =>
    5.21 +                    if Long_Name.is_qualified c
    5.22 +                    then (report ps (markup_const ctxt) c; Const (c, T))
    5.23 +                    else (report ps (markup_free ctxt) c; Free (c, T))))
    5.24            | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
    5.25            | decode ps _ bs (t as Bound i) =
    5.26                (case try (nth bs) i of
    5.27 @@ -322,8 +323,7 @@
    5.28  
    5.29      val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
    5.30        handle ERROR msg =>
    5.31 -        error (msg ^
    5.32 -          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
    5.33 +        error (msg ^ implode (map (Markup.markup_report o Lexicon.reported_token_range ctxt) toks));
    5.34      val len = length pts;
    5.35  
    5.36      val limit = Config.get ctxt Syntax.ambiguity_limit;
    5.37 @@ -355,7 +355,7 @@
    5.38  
    5.39  fun parse_failed ctxt pos msg kind =
    5.40    cat_error msg ("Failed to parse " ^ kind ^
    5.41 -    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
    5.42 +    Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
    5.43  
    5.44  fun parse_sort ctxt =
    5.45    Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort

     6.1 --- a/src/Pure/consts.ML	Thu Mar 06 14:38:54 2014 +0100
     6.2 +++ b/src/Pure/consts.ML	Thu Mar 06 16:12:26 2014 +0100
     6.3 @@ -25,7 +25,7 @@
     6.4    val extern: Proof.context -> T -> string -> xstring
     6.5    val intern_syntax: T -> xstring -> string
     6.6    val extern_syntax: Proof.context -> T -> string -> xstring
     6.7 -  val check_const: Context.generic -> T -> xstring * Position.T -> term * Position.report list
     6.8 +  val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
     6.9    val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    6.10    val typargs: T -> string * typ -> typ list
    6.11    val instance: T -> string * typ list -> typ
    6.12 @@ -143,11 +143,11 @@
    6.13  
    6.14  (* check_const *)
    6.15  
    6.16 -fun check_const context consts (xname, pos) =
    6.17 +fun check_const context consts (xname, ps) =
    6.18    let
    6.19      val Consts {decls, ...} = consts;
    6.20 -    val ((c, reports), _) = Name_Space.check_reports context decls (xname, pos);
    6.21 -    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
    6.22 +    val ((c, reports), _) = Name_Space.check_reports context decls (xname, ps);
    6.23 +    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here_list ps);
    6.24    in (Const (c, T), reports) end;
    6.25  
    6.26  

     7.1 --- a/src/Pure/type.ML	Thu Mar 06 14:38:54 2014 +0100
     7.2 +++ b/src/Pure/type.ML	Thu Mar 06 16:12:26 2014 +0100
     7.3 @@ -259,7 +259,8 @@
     7.4  
     7.5  fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
     7.6  
     7.7 -fun check_decl context (TSig {types, ...}) = Name_Space.check_reports context types;
     7.8 +fun check_decl context (TSig {types, ...}) (c, pos) =
     7.9 +  Name_Space.check_reports context types (c, [pos]);
    7.10  
    7.11  fun the_decl tsig (c, pos) =
    7.12    (case lookup_type tsig c of