# HG changeset patch # User wenzelm # Date 1394118746 -3600 # Node ID 94d384d621b0673c871c6208757ed26b7eb62a87 # Parent e8f1bf005661c5462945c760d3ff145cc054438d reject internal term names outright, and complete consts instead; more general Name_Space.check_reports; more compact Markup.markup_report; diff -r e8f1bf005661 -r 94d384d621b0 src/Pure/General/name_space.ML --- 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; diff -r e8f1bf005661 -r 94d384d621b0 src/Pure/Isar/args.ML --- 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 = diff -r e8f1bf005661 -r 94d384d621b0 src/Pure/Isar/proof_context.ML --- 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, _)) => diff -r e8f1bf005661 -r 94d384d621b0 src/Pure/PIDE/markup.ML --- 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; diff -r e8f1bf005661 -r 94d384d621b0 src/Pure/Syntax/syntax_phases.ML --- 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 diff -r e8f1bf005661 -r 94d384d621b0 src/Pure/consts.ML --- 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; diff -r e8f1bf005661 -r 94d384d621b0 src/Pure/type.ML --- 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