# HG changeset patch # User wenzelm # Date 1394123852 -3600 # Node ID c3b458435f4f07aff794fbe1887c347d323ae329 # Parent 4ec984df4f45c4aeef816fb4fda5420283148639 more decisive commitment to get_free vs. the_const; tuned; diff -r 4ec984df4f45 -r c3b458435f4f src/Pure/General/position.ML --- a/src/Pure/General/position.ML Thu Mar 06 16:33:48 2014 +0100 +++ b/src/Pure/General/position.ML Thu Mar 06 17:37:32 2014 +0100 @@ -43,6 +43,7 @@ val reports: report list -> unit val store_reports: report_text list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit + val append_reports: report_text list Unsynchronized.ref -> report list -> unit val here: T -> string val here_list: T list -> string type range = T * T @@ -182,6 +183,9 @@ let val ms = markup x in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end; +fun append_reports (r: report_text list Unsynchronized.ref) reports = + Unsynchronized.change r (append (map (rpair "") reports)); + (* here: inlined formal markup *) diff -r 4ec984df4f45 -r c3b458435f4f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 06 16:33:48 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 06 17:37:32 2014 +0100 @@ -73,7 +73,7 @@ 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 + xstring * Position.T list -> term * Position.report list val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term val read_arity: Proof.context -> xstring * string list * string -> arity val cert_arity: Proof.context -> arity -> arity @@ -476,31 +476,31 @@ |> implode |> Markup.markup_report; -fun check_const ctxt {proper, strict} (c, pos) = +fun check_const ctxt {proper, strict} (c, ps) = 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); + Name.reject_internal (c, ps) handle ERROR msg => + error (msg ^ consts_completion_message ctxt (c, ps)); + fun err msg = error (msg ^ Position.here_list ps); val consts = consts_of ctxt; val fixed = if proper then NONE else Variable.lookup_fixed ctxt c; val (t, reports) = (case (fixed, Variable.lookup_const ctxt c) of (SOME x, NONE) => let - 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))] - else []; + val reports = ps + |> filter (Context_Position.is_reported ctxt) + |> map (fn pos => + (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))); in (Free (x, infer_type ctxt (x, dummyT)), reports) end | (_, SOME d) => let val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg; - val reports = - if Context_Position.is_reported ctxt pos - then [(pos, Name_Space.markup (Consts.space_of consts) d)] else []; + val reports = ps + |> filter (Context_Position.is_reported ctxt) + |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d)); in (Const (d, T), reports) end - | _ => Consts.check_const (Context.Proof ctxt) consts (c, [pos])); + | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps)); val _ = (case (strict, t) of (true, Const (d, _)) => @@ -510,8 +510,8 @@ fun read_const ctxt flags text = let - val (t, reports) = - check_const ctxt flags (Symbol_Pos.source_content (Syntax.read_token text)); + val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text); + val (t, reports) = check_const ctxt flags (xname, [pos]); val _ = Position.reports reports; in t end; diff -r 4ec984df4f45 -r c3b458435f4f src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 16:33:48 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 17:37:32 2014 +0100 @@ -140,6 +140,7 @@ let val reports = Unsynchronized.ref ([]: Position.report_text list); fun report pos = Position.store_reports reports [pos]; + val append_reports = Position.append_reports reports; fun trans a args = (case trf a of @@ -164,7 +165,7 @@ let val pos = Lexicon.pos_of_token tok; val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos); - val _ = Unsynchronized.change reports (append (map (rpair "") rs)); + val _ = append_reports rs; in [Ast.Constant (Lexicon.mark_class c)] end | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = let @@ -172,7 +173,7 @@ val (Type (c, _), rs) = Proof_Context.check_type_name ctxt {proper = true, strict = false} (Lexicon.str_of_token tok, pos); - val _ = Unsynchronized.change reports (append (map (rpair "") rs)); + val _ = append_reports 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 @@ -221,22 +222,23 @@ (* decode_term -- transform parse tree into raw term *) -fun decode_const ctxt c = +fun decode_const ctxt (c, ps) = let - val (Const (c', _), _) = - Proof_Context.check_const ctxt {proper = true, strict = false} (c, Position.none); - in c' end; + val (Const (c', _), reports) = + Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps); + in (c', reports) end; fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result | decode_term ctxt (reports0, Exn.Res tm) = let - fun get_const c = - (true, decode_const ctxt c) handle ERROR _ => - (false, Consts.intern (Proof_Context.consts_of ctxt) c); + val reports = Unsynchronized.ref reports0; + fun report ps = Position.store_reports reports ps; + val append_reports = Position.append_reports reports; + fun get_free x = let val fixed = Variable.lookup_fixed ctxt x; - val is_const = can (decode_const ctxt) x orelse Long_Name.is_qualified x; + val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x; val is_declared = is_some (Variable.def_type ctxt false (x, ~1)); in if Variable.is_const ctxt x then NONE @@ -245,8 +247,11 @@ else NONE end; - val reports = Unsynchronized.ref reports0; - fun report ps = Position.store_reports reports ps; + fun the_const (a, ps) = + let + val (c, rs) = decode_const ctxt (a, ps); + val _ = append_reports rs; + in c end; fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = (case Term_Position.decode_position typ of @@ -269,20 +274,15 @@ let val c = (case try Lexicon.unmark_const a of - SOME c => c - | NONE => snd (get_const a)); - val _ = report ps (markup_const ctxt) c; + SOME c => (report ps (markup_const ctxt) c; c) + | NONE => the_const (a, ps)); in Const (c, T) end) | decode ps _ _ (Free (a, 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)))) + (case get_free a of + SOME x => (report ps (markup_free ctxt) x; Free (x, T)) + | NONE => Const (the_const (a, ps), 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 @@ -813,7 +813,7 @@ fun const_ast_tr intern ctxt [Ast.Variable c] = let - val c' = decode_const ctxt c; + val (c', _) = decode_const ctxt (c, []); val d = if intern then Lexicon.mark_const c' else c; in Ast.Constant d end | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =