reject internal term names outright, and complete consts instead;
more general Name_Space.check_reports;
more compact Markup.markup_report;
--- a/src/Pure/General/name_space.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/General/name_space.ML Thu Mar 06 16:12:26 2014 +0100
@@ -56,7 +56,7 @@
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
+ xstring * Position.T list -> (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
@@ -446,24 +446,27 @@
type 'a table = T * 'a Symtab.table;
-fun check_reports context (space, tab) (xname, pos) =
+fun check_reports context (space, tab) (xname, ps) =
let val name = intern space xname in
(case Symtab.lookup tab name of
SOME x =>
let
val reports =
- if Context_Position.is_reported_generic context pos
- then [(pos, markup space name)] else [];
+ filter (Context_Position.is_reported_generic context) ps
+ |> map (fn pos => (pos, markup space name));
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)))))
+ let
+ val completions = map (fn pos => completion context space (xname, pos)) ps;
+ in
+ error (undefined (kind_of space) name ^ Position.here_list ps ^
+ implode (map (Markup.markup_report o Completion.reported_text) completions))
+ end)
end;
-fun check context table arg =
+fun check context table (xname, pos) =
let
- val ((name, reports), x) = check_reports context table arg;
+ val ((name, reports), x) = check_reports context table (xname, [pos]);
val _ = Position.reports reports;
in (name, x) end;
--- a/src/Pure/Isar/args.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/Isar/args.ML Thu Mar 06 16:12:26 2014 +0100
@@ -299,7 +299,7 @@
| (_, (_, args2)) =>
error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
(if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2)) ^
- Markup.markup Markup.report (reported_text ())))
+ Markup.markup_report (reported_text ())))
end;
fun context_syntax kind scan src =
--- a/src/Pure/Isar/proof_context.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 06 16:12:26 2014 +0100
@@ -71,6 +71,7 @@
val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
xstring * Position.T -> typ * Position.report list
val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
+ val consts_completion_message: Proof.context -> xstring * Position.T list -> string
val check_const: Proof.context -> {proper: bool, strict: bool} ->
xstring * Position.T -> term * Position.report list
val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
@@ -384,9 +385,8 @@
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))));
+ Markup.markup_report (Completion.reported_text
+ (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
val reports =
if Context_Position.is_reported ctxt pos
then [(pos, Name_Space.markup class_space name)] else [];
@@ -469,8 +469,18 @@
(* constant names *)
+fun consts_completion_message ctxt (c, ps) =
+ ps |> map (fn pos =>
+ Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
+ |> Completion.reported_text)
+ |> implode
+ |> Markup.markup_report;
+
fun check_const ctxt {proper, strict} (c, pos) =
let
+ val _ =
+ Name.reject_internal (c, [pos]) handle ERROR msg =>
+ error (msg ^ consts_completion_message ctxt (c, [pos]));
fun err msg = error (msg ^ Position.here pos);
val consts = consts_of ctxt;
val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
@@ -478,7 +488,6 @@
(case (fixed, Variable.lookup_const ctxt c) of
(SOME x, NONE) =>
let
- val _ = Name.reject_internal (c, [pos]);
val reports =
if Context_Position.is_reported ctxt pos then
[(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
@@ -491,7 +500,7 @@
if Context_Position.is_reported ctxt pos
then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
in (Const (d, T), reports) end
- | _ => Consts.check_const (Context.Proof ctxt) consts (c, pos));
+ | _ => Consts.check_const (Context.Proof ctxt) consts (c, [pos]));
val _ =
(case (strict, t) of
(true, Const (d, _)) =>
--- a/src/Pure/PIDE/markup.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Thu Mar 06 16:12:26 2014 +0100
@@ -189,6 +189,7 @@
val enclose: T -> Output.output -> Output.output
val markup: T -> string -> string
val markup_only: T -> string
+ val markup_report: string -> string
end;
structure Markup: MARKUP =
@@ -602,4 +603,7 @@
fun markup_only m = markup m "";
+fun markup_report "" = ""
+ | markup_report txt = markup report txt;
+
end;
--- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 16:12:26 2014 +0100
@@ -274,14 +274,15 @@
val _ = report ps (markup_const ctxt) c;
in Const (c, T) end)
| decode ps _ _ (Free (a, T)) =
- (Name.reject_internal (a, ps);
- case (get_free a, get_const a) of
- (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
- | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
- | (_, (false, c)) =>
- if Long_Name.is_qualified c
- then (report ps (markup_const ctxt) c; Const (c, T))
- else (report ps (markup_free ctxt) c; Free (c, T)))
+ ((Name.reject_internal (a, ps) handle ERROR msg =>
+ error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
+ (case (get_free a, get_const a) of
+ (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
+ | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
+ | (_, (false, c)) =>
+ if Long_Name.is_qualified c
+ then (report ps (markup_const ctxt) c; Const (c, T))
+ else (report ps (markup_free ctxt) c; Free (c, T))))
| decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
| decode ps _ bs (t as Bound i) =
(case try (nth bs) i of
@@ -322,8 +323,7 @@
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
- error (msg ^
- implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
+ error (msg ^ implode (map (Markup.markup_report o Lexicon.reported_token_range ctxt) toks));
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;
@@ -355,7 +355,7 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
+ Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
fun parse_sort ctxt =
Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
--- a/src/Pure/consts.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/consts.ML Thu Mar 06 16:12:26 2014 +0100
@@ -25,7 +25,7 @@
val extern: Proof.context -> T -> string -> xstring
val intern_syntax: T -> xstring -> string
val extern_syntax: Proof.context -> T -> string -> xstring
- val check_const: Context.generic -> T -> xstring * Position.T -> term * Position.report list
+ val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
@@ -143,11 +143,11 @@
(* check_const *)
-fun check_const context consts (xname, pos) =
+fun check_const context consts (xname, ps) =
let
val Consts {decls, ...} = consts;
- val ((c, reports), _) = Name_Space.check_reports context decls (xname, pos);
- val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
+ val ((c, reports), _) = Name_Space.check_reports context decls (xname, ps);
+ val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here_list ps);
in (Const (c, T), reports) end;
--- a/src/Pure/type.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/type.ML Thu Mar 06 16:12:26 2014 +0100
@@ -259,7 +259,8 @@
fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
-fun check_decl context (TSig {types, ...}) = Name_Space.check_reports context types;
+fun check_decl context (TSig {types, ...}) (c, pos) =
+ Name_Space.check_reports context types (c, [pos]);
fun the_decl tsig (c, pos) =
(case lookup_type tsig c of