# HG changeset patch # User wenzelm # Date 1535651976 -7200 # Node ID 9207ada0ca3164bb0a8257d7a7b4719598a837db # Parent 8825efd1c2cff1ad6cbda51a2ed4c000bb546be4# Parent e1796b8ddbae534055428c4fe898654a5ead6498 merged diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/General/position.ML Thu Aug 30 19:59:36 2018 +0200 @@ -29,6 +29,7 @@ val id_only: string -> T val get_id: T -> string option val put_id: string -> T -> T + val copy_id: T -> T -> T val id_properties_of: T -> Properties.T val parse_id: T -> int option val adjust_offsets: (int -> int option) -> T -> T @@ -142,6 +143,7 @@ fun get_id (Pos (_, props)) = Properties.get props Markup.idN; fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props)); +fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id); fun parse_id pos = Option.map Value.parse_int (get_id pos); @@ -151,14 +153,16 @@ | NONE => []); fun adjust_offsets adjust (pos as Pos (_, props)) = - (case parse_id pos of - SOME id => - (case adjust id of - SOME offset => - let val Pos (count, _) = advance_offsets offset pos - in Pos (count, Properties.remove Markup.idN props) end - | NONE => pos) - | NONE => pos); + if is_none (file_of pos) then + (case parse_id pos of + SOME id => + (case adjust id of + SOME offset => + let val Pos (count, _) = advance_offsets offset pos + in Pos (count, Properties.remove Markup.idN props) end + | NONE => pos) + | NONE => pos) + else pos; (* markup properties *) diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/Isar/class.ML Thu Aug 30 19:59:36 2018 +0200 @@ -229,9 +229,13 @@ fun activate_defs class thms thy = (case Element.eq_morphism thy thms of - SOME eq_morph => fold (fn cls => fn thy => - Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) - (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy + SOME eq_morph => + fold (fn cls => fn thy => + Context.theory_map + (Locale.amend_registration + {dep = (cls, base_morphism thy cls), + mixin = SOME (eq_morph, true), + export = export_morphism thy cls}) thy) (heritage thy [class]) thy | NONE => thy); fun register_operation class (c, t) input_only thy = @@ -484,10 +488,13 @@ val diff_sort = Sign.complete_sort thy [sup] |> subtract (op =) (Sign.complete_sort thy [sub]) |> filter (is_class thy); - fun add_dependency some_wit = case some_dep_morph of - SOME dep_morph => Generic_Target.locale_dependency sub - (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export - | NONE => I; + fun add_dependency some_wit (* FIXME unused!? *) = + (case some_dep_morph of + SOME dep_morph => + Generic_Target.locale_dependency sub + {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)), + mixin = NONE, export = export} + | NONE => I); in lthy |> Local_Theory.raw_theory diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/Isar/class_declaration.ML Thu Aug 30 19:59:36 2018 +0200 @@ -328,8 +328,10 @@ |-> (fn (param_map, params, assm_axiom) => `(fn thy => calculate thy class sups base_sort param_map assm_axiom) #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) => - Context.theory_map (Locale.add_registration (class, base_morph) - (Option.map (rpair true) eq_morph) export_morph) + Locale.add_registration_theory + {dep = (class, base_morph), + mixin = Option.map (rpair true) eq_morph, + export = export_morph} #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) |> snd diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/Isar/generic_target.ML Thu Aug 30 19:59:36 2018 +0200 @@ -52,8 +52,7 @@ val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val theory_declaration: declaration -> local_theory -> local_theory - val theory_registration: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory + val theory_registration: Locale.registration -> local_theory -> local_theory (*locale target primitives*) val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list -> @@ -71,8 +70,7 @@ local_theory -> local_theory val locale_const: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory - val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory + val locale_dependency: string -> Locale.registration -> local_theory -> local_theory (*initialisation*) val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context, @@ -372,7 +370,7 @@ background_declaration decl #> standard_declaration (K true) decl; val theory_registration = - Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration; + Local_Theory.raw_theory o Locale.add_registration_theory; @@ -406,9 +404,9 @@ locale_target_const locale (K true) prmode ((b, mx), rhs) #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); -fun locale_dependency locale dep_morph mixin export = - (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export - #> Locale.activate_fragment_nonbrittle dep_morph mixin export; +fun locale_dependency locale registration = + Local_Theory.raw_theory (Locale.add_dependency locale registration) + #> Locale.add_registration_local_theory registration; (** locale abbreviations **) diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/Isar/interpretation.ML Thu Aug 30 19:59:36 2018 +0200 @@ -97,30 +97,30 @@ local -fun meta_rewrite eqns ctxt = +fun abs_def_rule eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); -fun note_eqns_register pos note activate deps eqnss witss def_eqns thms export export' ctxt = +fun note_eqns_register note add_registration + deps eqnss witss def_eqns thms export export' ctxt = let - val thmss = unflat ((map o map) fst eqnss) thms; - val factss = - map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss; - val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt; + val factss = thms + |> unflat ((map o map) #1 eqnss) + |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss); + val (eqnss', ctxt') = + fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt; val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); - val (eqns', ctxt'') = ctxt' - |> note Thm.theoremK [defs] - |-> meta_rewrite; - val dep_morphs = - map2 (fn (dep, morph) => fn wits => - let val morph' = morph - $> Element.satisfy_morphism (map (Element.transform_witness export') wits) - $> Morphism.binding_morphism "position" (Binding.set_pos pos) - in (dep, morph') end) deps witss; - fun activate' (dep_morph, eqns) ctxt = - activate dep_morph - (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns'))) - export ctxt; - in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end; + val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule; + val deps' = + (deps ~~ witss) |> map (fn ((dep, morph), wits) => + (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))); + fun register (dep, eqns) ctxt = + ctxt |> add_registration + {dep = dep, + mixin = + Option.map (rpair true) + (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')), + export = export}; + in ctxt'' |> fold register (deps' ~~ eqnss') end; in @@ -129,9 +129,8 @@ let val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = prep_interpretation expression raw_defs initial_ctxt; - val pos = Position.thread_data (); fun after_qed witss eqns = - note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export'; + note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export'; in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; end; @@ -143,23 +142,16 @@ local +fun setup_proof state after_qed propss eqns goal_ctxt = + Element.witness_local_proof_eqs + (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts) + "interpret" propss eqns goal_ctxt state; + fun gen_interpret prep_interpretation expression state = - let - val _ = Proof.assert_forward_or_chain state; - fun lift_after_qed after_qed witss eqns = - Proof.map_context (after_qed witss eqns) #> Proof.reset_facts; - fun setup_proof after_qed propss eqns goal_ctxt = - Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" - propss eqns goal_ctxt state; - fun add_registration reg mixin export ctxt = ctxt - |> Proof_Context.set_stmt false - |> Context.proof_map (Locale.add_registration reg mixin export) - |> Proof_Context.restore_stmt ctxt; - in - Proof.context_of state - |> generic_interpretation prep_interpretation setup_proof - Attrib.local_notes add_registration expression [] - end; + Proof.assert_forward_or_chain state + |> Proof.context_of + |> generic_interpretation prep_interpretation (setup_proof state) + Attrib.local_notes Locale.add_registration_proof expression []; in diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/Isar/local_theory.ML Thu Aug 30 19:59:36 2018 +0200 @@ -14,6 +14,11 @@ type fact = binding * thms; end; +structure Locale = +struct + type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}; +end; + signature LOCAL_THEORY = sig type operations @@ -54,10 +59,8 @@ val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory - val theory_registration: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory - val locale_dependency: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory + val theory_registration: Locale.registration -> local_theory -> local_theory + val locale_dependency: Locale.registration -> local_theory -> local_theory val pretty: local_theory -> Pretty.T list val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory val set_defsort: sort -> local_theory -> local_theory @@ -91,10 +94,8 @@ abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory, declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory, - theory_registration: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory, - locale_dependency: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory, + theory_registration: Locale.registration -> local_theory -> local_theory, + locale_dependency: Locale.registration -> local_theory -> local_theory, pretty: local_theory -> Pretty.T list}; type lthy = @@ -276,10 +277,10 @@ val define_internal = operation2 #define true; val notes_kind = operation2 #notes; val declaration = operation2 #declaration; -fun theory_registration dep_morph mixin export = - assert_bottom #> operation (fn ops => #theory_registration ops dep_morph mixin export); -fun locale_dependency dep_morph mixin export = - assert_bottom #> operation (fn ops => #locale_dependency ops dep_morph mixin export); +fun theory_registration registration = + assert_bottom #> operation (fn ops => #theory_registration ops registration); +fun locale_dependency registration = + assert_bottom #> operation (fn ops => #locale_dependency ops registration); (* theorems *) diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/Isar/locale.ML Thu Aug 30 19:59:36 2018 +0200 @@ -73,17 +73,15 @@ val intro_locales_tac: bool -> Proof.context -> thm list -> tactic (* Registrations and dependencies *) - val add_registration: string * morphism -> (morphism * bool) option -> - morphism -> Context.generic -> Context.generic - val activate_fragment: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory - val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory - val amend_registration: string * morphism -> morphism * bool -> - morphism -> Context.generic -> Context.generic + type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism} + val amend_registration: registration -> Context.generic -> Context.generic + val add_registration: registration -> Context.generic -> Context.generic + val add_registration_theory: registration -> theory -> theory + val add_registration_proof: registration -> Proof.context -> Proof.context + val add_registration_local_theory: registration -> local_theory -> local_theory + val activate_fragment: registration -> local_theory -> local_theory val registrations_of: Context.generic -> string -> (string * morphism) list - val add_dependency: string -> string * morphism -> (morphism * bool) option -> - morphism -> theory -> theory + val add_dependency: string -> registration -> theory -> theory (* Diagnostic *) val hyp_spec_of: theory -> string -> Element.context_i list @@ -516,60 +514,68 @@ (*** Add and extend registrations ***) -fun amend_registration (name, morph) mixin export context = - let - val thy = Context.theory_of context; - val ctxt = Context.proof_of context; +type registration = Locale.registration; + +fun amend_registration {mixin = NONE, ...} context = context + | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context = + let + val thy = Context.theory_of context; + val ctxt = Context.proof_of context; - val regs = Registrations.get context |> fst; - val base = instance_of thy name (morph $> export); - val serial' = - (case Idtab.lookup regs (name, base) of - NONE => - error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^ - " with\nparameter instantiation " ^ - space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ - " available") - | SOME (_, serial') => serial'); - in - add_mixin serial' mixin context - end; + val regs = Registrations.get context |> fst; + val base = instance_of thy name (morph $> export); + val serial' = + (case Idtab.lookup regs (name, base) of + NONE => + error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^ + " with\nparameter instantiation " ^ + space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ + " available") + | SOME (_, serial') => serial'); + in + add_mixin serial' mixin context + end; (* Note that a registration that would be subsumed by an existing one will not be generated, and it will not be possible to amend it. *) -fun add_registration (name, base_morph) mixin export context = +fun add_registration {dep = (name, base_morph), mixin, export} context = let val thy = Context.theory_of context; - val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix); - val morph = base_morph $> mix; - val inst = instance_of thy name morph; + val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ())); + val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix); + val inst = instance_of thy name mix_morph; val idents = Idents.get context; in - if redundant_ident thy idents (name, inst) - then context (* FIXME amend mixins? *) + if redundant_ident thy idents (name, inst) then context (* FIXME amend mixins? *) else (idents, context) (* add new registrations with inherited mixins *) - |> roundup thy (add_reg thy export) export (name, morph) - |> snd + |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2 (* add mixin *) - |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export) + |> amend_registration {dep = (name, mix_morph), mixin = mixin, export = export} (* activate import hierarchy as far as not already active *) - |> activate_facts (SOME export) (name, morph) + |> activate_facts (SOME export) (name, mix_morph $> pos_morph) + end; + +val add_registration_theory = Context.theory_map o add_registration; + +fun add_registration_proof registration ctxt = ctxt + |> Proof_Context.set_stmt false + |> Context.proof_map (add_registration registration) + |> Proof_Context.restore_stmt ctxt; + +fun add_registration_local_theory registration lthy = + let val n = Local_Theory.level lthy in + lthy |> Local_Theory.map_contexts (fn level => + level = n - 1 ? Context.proof_map (add_registration registration)) end; (* locale fragments within local theory *) -fun activate_fragment_nonbrittle dep_morph mixin export lthy = - let val n = Local_Theory.level lthy in - lthy |> Local_Theory.map_contexts (fn level => - level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export)) - end; - -fun activate_fragment dep_morph mixin export = - Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export; +fun activate_fragment registration = + Local_Theory.mark_brittle #> add_registration_local_theory registration; @@ -590,7 +596,7 @@ end; *) -fun add_dependency loc (name, morph) mixin export thy = +fun add_dependency loc {dep = (name, morph), mixin, export} thy = let val serial' = serial (); val thy' = thy |> @@ -603,7 +609,7 @@ (registrations_of context' loc) (Idents.get context', []); in thy' - |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs + |> fold_rev (fn dep => add_registration_theory {dep = dep, mixin = NONE, export = export}) regs end; diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/PIDE/command.ML Thu Aug 30 19:59:36 2018 +0200 @@ -70,7 +70,8 @@ val text = File.read full_path; val lines = split_lines text; val digest = SHA1.digest text; - in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end + val file_pos = Position.copy_id pos (Path.position full_path); + in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end handle ERROR msg => error (msg ^ Position.here pos); val read_file = read_file_node ""; diff -r 8825efd1c2cf -r 9207ada0ca31 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 30 18:40:53 2018 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 30 19:59:36 2018 +0200 @@ -706,14 +706,16 @@ def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail) def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) + def lookup_id(id: Document_ID.Generic): Option[Command.State] = + commands.get(id) orElse execs.get(id) + private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean = id == st.command.id || (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false }) private def other_id(id: Document_ID.Generic) : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = - (execs.get(id) orElse commands.get(id)).map(st => - ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk))) + lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk))) private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] = (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) => @@ -1077,7 +1079,7 @@ /* find command */ def find_command(id: Document_ID.Generic): Option[(Node, Command)] = - state.commands.get(id) orElse state.execs.get(id) match { + state.lookup_id(id) match { case None => None case Some(st) => val command = st.command