merged
authorwenzelm
Thu Aug 30 19:59:36 2018 +0200 (13 months ago)
changeset 688599207ada0ca31
parent 68848 8825efd1c2cf
parent 68858 e1796b8ddbae
child 68860 f443ec10447d
child 68861 2d99562a7fe2
merged
     1.1 --- a/src/Pure/General/position.ML	Thu Aug 30 18:40:53 2018 +0200
     1.2 +++ b/src/Pure/General/position.ML	Thu Aug 30 19:59:36 2018 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val id_only: string -> T
     1.5    val get_id: T -> string option
     1.6    val put_id: string -> T -> T
     1.7 +  val copy_id: T -> T -> T
     1.8    val id_properties_of: T -> Properties.T
     1.9    val parse_id: T -> int option
    1.10    val adjust_offsets: (int -> int option) -> T -> T
    1.11 @@ -142,6 +143,7 @@
    1.12  
    1.13  fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
    1.14  fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
    1.15 +fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
    1.16  
    1.17  fun parse_id pos = Option.map Value.parse_int (get_id pos);
    1.18  
    1.19 @@ -151,14 +153,16 @@
    1.20    | NONE => []);
    1.21  
    1.22  fun adjust_offsets adjust (pos as Pos (_, props)) =
    1.23 -  (case parse_id pos of
    1.24 -    SOME id =>
    1.25 -      (case adjust id of
    1.26 -        SOME offset =>
    1.27 -          let val Pos (count, _) = advance_offsets offset pos
    1.28 -          in Pos (count, Properties.remove Markup.idN props) end
    1.29 -      | NONE => pos)
    1.30 -  | NONE => pos);
    1.31 +  if is_none (file_of pos) then
    1.32 +    (case parse_id pos of
    1.33 +      SOME id =>
    1.34 +        (case adjust id of
    1.35 +          SOME offset =>
    1.36 +            let val Pos (count, _) = advance_offsets offset pos
    1.37 +            in Pos (count, Properties.remove Markup.idN props) end
    1.38 +        | NONE => pos)
    1.39 +    | NONE => pos)
    1.40 +  else pos;
    1.41  
    1.42  
    1.43  (* markup properties *)
     2.1 --- a/src/Pure/Isar/class.ML	Thu Aug 30 18:40:53 2018 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Thu Aug 30 19:59:36 2018 +0200
     2.3 @@ -229,9 +229,13 @@
     2.4  
     2.5  fun activate_defs class thms thy =
     2.6    (case Element.eq_morphism thy thms of
     2.7 -    SOME eq_morph => fold (fn cls => fn thy =>
     2.8 -      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
     2.9 -        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
    2.10 +    SOME eq_morph =>
    2.11 +      fold (fn cls => fn thy =>
    2.12 +        Context.theory_map
    2.13 +          (Locale.amend_registration
    2.14 +            {dep = (cls, base_morphism thy cls),
    2.15 +              mixin = SOME (eq_morph, true),
    2.16 +              export = export_morphism thy cls}) thy) (heritage thy [class]) thy
    2.17    | NONE => thy);
    2.18  
    2.19  fun register_operation class (c, t) input_only thy =
    2.20 @@ -484,10 +488,13 @@
    2.21      val diff_sort = Sign.complete_sort thy [sup]
    2.22        |> subtract (op =) (Sign.complete_sort thy [sub])
    2.23        |> filter (is_class thy);
    2.24 -    fun add_dependency some_wit = case some_dep_morph of
    2.25 -        SOME dep_morph => Generic_Target.locale_dependency sub
    2.26 -          (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)) NONE export
    2.27 -      | NONE => I;
    2.28 +    fun add_dependency some_wit (* FIXME unused!? *) =
    2.29 +      (case some_dep_morph of
    2.30 +        SOME dep_morph =>
    2.31 +          Generic_Target.locale_dependency sub
    2.32 +            {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
    2.33 +              mixin = NONE, export = export}
    2.34 +      | NONE => I);
    2.35    in
    2.36      lthy
    2.37      |> Local_Theory.raw_theory
     3.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Aug 30 18:40:53 2018 +0200
     3.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 30 19:59:36 2018 +0200
     3.3 @@ -328,8 +328,10 @@
     3.4      |-> (fn (param_map, params, assm_axiom) =>
     3.5         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     3.6      #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
     3.7 -       Context.theory_map (Locale.add_registration (class, base_morph)
     3.8 -         (Option.map (rpair true) eq_morph) export_morph)
     3.9 +       Locale.add_registration_theory
    3.10 +         {dep = (class, base_morph),
    3.11 +           mixin = Option.map (rpair true) eq_morph,
    3.12 +           export = export_morph}
    3.13      #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
    3.14      #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
    3.15      |> snd
     4.1 --- a/src/Pure/Isar/generic_target.ML	Thu Aug 30 18:40:53 2018 +0200
     4.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Aug 30 19:59:36 2018 +0200
     4.3 @@ -52,8 +52,7 @@
     4.4    val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
     4.5      local_theory -> (term * term) * local_theory
     4.6    val theory_declaration: declaration -> local_theory -> local_theory
     4.7 -  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     4.8 -    local_theory -> local_theory
     4.9 +  val theory_registration: Locale.registration -> local_theory -> local_theory
    4.10  
    4.11    (*locale target primitives*)
    4.12    val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
    4.13 @@ -71,8 +70,7 @@
    4.14      local_theory -> local_theory
    4.15    val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
    4.16      local_theory -> local_theory
    4.17 -  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
    4.18 -    local_theory -> local_theory
    4.19 +  val locale_dependency: string -> Locale.registration -> local_theory -> local_theory
    4.20  
    4.21    (*initialisation*)
    4.22    val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
    4.23 @@ -372,7 +370,7 @@
    4.24    background_declaration decl #> standard_declaration (K true) decl;
    4.25  
    4.26  val theory_registration =
    4.27 -  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    4.28 +  Local_Theory.raw_theory o Locale.add_registration_theory;
    4.29  
    4.30  
    4.31  
    4.32 @@ -406,9 +404,9 @@
    4.33    locale_target_const locale (K true) prmode ((b, mx), rhs)
    4.34    #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
    4.35  
    4.36 -fun locale_dependency locale dep_morph mixin export =
    4.37 -  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
    4.38 -  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
    4.39 +fun locale_dependency locale registration =
    4.40 +  Local_Theory.raw_theory (Locale.add_dependency locale registration)
    4.41 +  #> Locale.add_registration_local_theory registration;
    4.42  
    4.43  
    4.44  (** locale abbreviations **)
     5.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 18:40:53 2018 +0200
     5.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 19:59:36 2018 +0200
     5.3 @@ -97,30 +97,30 @@
     5.4  
     5.5  local
     5.6  
     5.7 -fun meta_rewrite eqns ctxt =
     5.8 +fun abs_def_rule eqns ctxt =
     5.9    (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
    5.10  
    5.11 -fun note_eqns_register pos note activate deps eqnss witss def_eqns thms export export' ctxt =
    5.12 +fun note_eqns_register note add_registration
    5.13 +    deps eqnss witss def_eqns thms export export' ctxt =
    5.14    let
    5.15 -    val thmss = unflat ((map o map) fst eqnss) thms;
    5.16 -    val factss =
    5.17 -      map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss;
    5.18 -    val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
    5.19 +    val factss = thms
    5.20 +      |> unflat ((map o map) #1 eqnss)
    5.21 +      |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
    5.22 +    val (eqnss', ctxt') =
    5.23 +      fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
    5.24      val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
    5.25 -    val (eqns', ctxt'') = ctxt'
    5.26 -      |> note Thm.theoremK [defs]
    5.27 -      |-> meta_rewrite;
    5.28 -    val dep_morphs =
    5.29 -      map2 (fn (dep, morph) => fn wits =>
    5.30 -        let val morph' = morph
    5.31 -          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
    5.32 -          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
    5.33 -        in (dep, morph') end) deps witss;
    5.34 -    fun activate' (dep_morph, eqns) ctxt =
    5.35 -      activate dep_morph
    5.36 -        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
    5.37 -        export ctxt;
    5.38 -  in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end;
    5.39 +    val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
    5.40 +    val deps' =
    5.41 +      (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
    5.42 +        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
    5.43 +    fun register (dep, eqns) ctxt =
    5.44 +      ctxt |> add_registration
    5.45 +        {dep = dep,
    5.46 +          mixin =
    5.47 +            Option.map (rpair true)
    5.48 +              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
    5.49 +          export = export};
    5.50 +  in ctxt'' |> fold register (deps' ~~ eqnss') end;
    5.51  
    5.52  in
    5.53  
    5.54 @@ -129,9 +129,8 @@
    5.55    let
    5.56      val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
    5.57        prep_interpretation expression raw_defs initial_ctxt;
    5.58 -    val pos = Position.thread_data ();
    5.59      fun after_qed witss eqns =
    5.60 -      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
    5.61 +      note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export';
    5.62    in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
    5.63  
    5.64  end;
    5.65 @@ -143,23 +142,16 @@
    5.66  
    5.67  local
    5.68  
    5.69 +fun setup_proof state after_qed propss eqns goal_ctxt =
    5.70 +  Element.witness_local_proof_eqs
    5.71 +    (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
    5.72 +    "interpret" propss eqns goal_ctxt state;
    5.73 +
    5.74  fun gen_interpret prep_interpretation expression state =
    5.75 -  let
    5.76 -    val _ = Proof.assert_forward_or_chain state;
    5.77 -    fun lift_after_qed after_qed witss eqns =
    5.78 -      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
    5.79 -    fun setup_proof after_qed propss eqns goal_ctxt =
    5.80 -      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
    5.81 -        propss eqns goal_ctxt state;
    5.82 -    fun add_registration reg mixin export ctxt = ctxt
    5.83 -      |> Proof_Context.set_stmt false
    5.84 -      |> Context.proof_map (Locale.add_registration reg mixin export)
    5.85 -      |> Proof_Context.restore_stmt ctxt;
    5.86 -  in
    5.87 -    Proof.context_of state
    5.88 -    |> generic_interpretation prep_interpretation setup_proof
    5.89 -      Attrib.local_notes add_registration expression []
    5.90 -  end;
    5.91 +  Proof.assert_forward_or_chain state
    5.92 +  |> Proof.context_of
    5.93 +  |> generic_interpretation prep_interpretation (setup_proof state)
    5.94 +    Attrib.local_notes Locale.add_registration_proof expression [];
    5.95  
    5.96  in
    5.97  
     6.1 --- a/src/Pure/Isar/local_theory.ML	Thu Aug 30 18:40:53 2018 +0200
     6.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Aug 30 19:59:36 2018 +0200
     6.3 @@ -14,6 +14,11 @@
     6.4    type fact = binding * thms;
     6.5  end;
     6.6  
     6.7 +structure Locale =
     6.8 +struct
     6.9 +  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism};
    6.10 +end;
    6.11 +
    6.12  signature LOCAL_THEORY =
    6.13  sig
    6.14    type operations
    6.15 @@ -54,10 +59,8 @@
    6.16    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    6.17      (term * term) * local_theory
    6.18    val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
    6.19 -  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    6.20 -    local_theory -> local_theory
    6.21 -  val locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
    6.22 -    local_theory -> local_theory
    6.23 +  val theory_registration: Locale.registration -> local_theory -> local_theory
    6.24 +  val locale_dependency: Locale.registration -> local_theory -> local_theory
    6.25    val pretty: local_theory -> Pretty.T list
    6.26    val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
    6.27    val set_defsort: sort -> local_theory -> local_theory
    6.28 @@ -91,10 +94,8 @@
    6.29    abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    6.30      (term * term) * local_theory,
    6.31    declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
    6.32 -  theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    6.33 -     local_theory -> local_theory,
    6.34 -  locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
    6.35 -     local_theory -> local_theory,
    6.36 +  theory_registration: Locale.registration -> local_theory -> local_theory,
    6.37 +  locale_dependency: Locale.registration -> local_theory -> local_theory,
    6.38    pretty: local_theory -> Pretty.T list};
    6.39  
    6.40  type lthy =
    6.41 @@ -276,10 +277,10 @@
    6.42  val define_internal = operation2 #define true;
    6.43  val notes_kind = operation2 #notes;
    6.44  val declaration = operation2 #declaration;
    6.45 -fun theory_registration dep_morph mixin export =
    6.46 -  assert_bottom #> operation (fn ops => #theory_registration ops dep_morph mixin export);
    6.47 -fun locale_dependency dep_morph mixin export =
    6.48 -  assert_bottom #> operation (fn ops => #locale_dependency ops dep_morph mixin export);
    6.49 +fun theory_registration registration =
    6.50 +  assert_bottom #> operation (fn ops => #theory_registration ops registration);
    6.51 +fun locale_dependency registration =
    6.52 +  assert_bottom #> operation (fn ops => #locale_dependency ops registration);
    6.53  
    6.54  
    6.55  (* theorems *)
     7.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 30 18:40:53 2018 +0200
     7.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 30 19:59:36 2018 +0200
     7.3 @@ -73,17 +73,15 @@
     7.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     7.5  
     7.6    (* Registrations and dependencies *)
     7.7 -  val add_registration: string * morphism -> (morphism * bool) option ->
     7.8 -    morphism -> Context.generic -> Context.generic
     7.9 -  val activate_fragment: string * morphism -> (morphism * bool) option -> morphism ->
    7.10 -    local_theory -> local_theory
    7.11 -  val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
    7.12 -    local_theory -> local_theory
    7.13 -  val amend_registration: string * morphism -> morphism * bool ->
    7.14 -    morphism -> Context.generic -> Context.generic
    7.15 +  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
    7.16 +  val amend_registration: registration -> Context.generic -> Context.generic
    7.17 +  val add_registration: registration -> Context.generic -> Context.generic
    7.18 +  val add_registration_theory: registration -> theory -> theory
    7.19 +  val add_registration_proof: registration -> Proof.context -> Proof.context
    7.20 +  val add_registration_local_theory: registration -> local_theory -> local_theory
    7.21 +  val activate_fragment: registration -> local_theory -> local_theory
    7.22    val registrations_of: Context.generic -> string -> (string * morphism) list
    7.23 -  val add_dependency: string -> string * morphism -> (morphism * bool) option ->
    7.24 -    morphism -> theory -> theory
    7.25 +  val add_dependency: string -> registration -> theory -> theory
    7.26  
    7.27    (* Diagnostic *)
    7.28    val hyp_spec_of: theory -> string -> Element.context_i list
    7.29 @@ -516,60 +514,68 @@
    7.30  
    7.31  (*** Add and extend registrations ***)
    7.32  
    7.33 -fun amend_registration (name, morph) mixin export context =
    7.34 -  let
    7.35 -    val thy = Context.theory_of context;
    7.36 -    val ctxt = Context.proof_of context;
    7.37 +type registration = Locale.registration;
    7.38 +
    7.39 +fun amend_registration {mixin = NONE, ...} context = context
    7.40 +  | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context =
    7.41 +      let
    7.42 +        val thy = Context.theory_of context;
    7.43 +        val ctxt = Context.proof_of context;
    7.44  
    7.45 -    val regs = Registrations.get context |> fst;
    7.46 -    val base = instance_of thy name (morph $> export);
    7.47 -    val serial' =
    7.48 -      (case Idtab.lookup regs (name, base) of
    7.49 -        NONE =>
    7.50 -          error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
    7.51 -            " with\nparameter instantiation " ^
    7.52 -            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    7.53 -            " available")
    7.54 -      | SOME (_, serial') => serial');
    7.55 -  in
    7.56 -    add_mixin serial' mixin context
    7.57 -  end;
    7.58 +        val regs = Registrations.get context |> fst;
    7.59 +        val base = instance_of thy name (morph $> export);
    7.60 +        val serial' =
    7.61 +          (case Idtab.lookup regs (name, base) of
    7.62 +            NONE =>
    7.63 +              error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
    7.64 +                " with\nparameter instantiation " ^
    7.65 +                space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    7.66 +                " available")
    7.67 +          | SOME (_, serial') => serial');
    7.68 +      in
    7.69 +        add_mixin serial' mixin context
    7.70 +      end;
    7.71  
    7.72  (* Note that a registration that would be subsumed by an existing one will not be
    7.73     generated, and it will not be possible to amend it. *)
    7.74  
    7.75 -fun add_registration (name, base_morph) mixin export context =
    7.76 +fun add_registration {dep = (name, base_morph), mixin, export} context =
    7.77    let
    7.78      val thy = Context.theory_of context;
    7.79 -    val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
    7.80 -    val morph = base_morph $> mix;
    7.81 -    val inst = instance_of thy name morph;
    7.82 +    val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ()));
    7.83 +    val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix);
    7.84 +    val inst = instance_of thy name mix_morph;
    7.85      val idents = Idents.get context;
    7.86    in
    7.87 -    if redundant_ident thy idents (name, inst)
    7.88 -    then context  (* FIXME amend mixins? *)
    7.89 +    if redundant_ident thy idents (name, inst) then context  (* FIXME amend mixins? *)
    7.90      else
    7.91        (idents, context)
    7.92        (* add new registrations with inherited mixins *)
    7.93 -      |> roundup thy (add_reg thy export) export (name, morph)
    7.94 -      |> snd
    7.95 +      |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2
    7.96        (* add mixin *)
    7.97 -      |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
    7.98 +      |> amend_registration {dep = (name, mix_morph), mixin = mixin, export = export}
    7.99        (* activate import hierarchy as far as not already active *)
   7.100 -      |> activate_facts (SOME export) (name, morph)
   7.101 +      |> activate_facts (SOME export) (name, mix_morph $> pos_morph)
   7.102 +  end;
   7.103 +
   7.104 +val add_registration_theory = Context.theory_map o add_registration;
   7.105 +
   7.106 +fun add_registration_proof registration ctxt = ctxt
   7.107 +  |> Proof_Context.set_stmt false
   7.108 +  |> Context.proof_map (add_registration registration)
   7.109 +  |> Proof_Context.restore_stmt ctxt;
   7.110 +
   7.111 +fun add_registration_local_theory registration lthy =
   7.112 +  let val n = Local_Theory.level lthy in
   7.113 +    lthy |> Local_Theory.map_contexts (fn level =>
   7.114 +      level = n - 1 ? Context.proof_map (add_registration registration))
   7.115    end;
   7.116  
   7.117  
   7.118  (* locale fragments within local theory *)
   7.119  
   7.120 -fun activate_fragment_nonbrittle dep_morph mixin export lthy =
   7.121 -  let val n = Local_Theory.level lthy in
   7.122 -    lthy |> Local_Theory.map_contexts (fn level =>
   7.123 -      level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export))
   7.124 -  end;
   7.125 -
   7.126 -fun activate_fragment dep_morph mixin export =
   7.127 -  Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export;
   7.128 +fun activate_fragment registration =
   7.129 +  Local_Theory.mark_brittle #> add_registration_local_theory registration;
   7.130  
   7.131  
   7.132  
   7.133 @@ -590,7 +596,7 @@
   7.134    end;
   7.135  *)
   7.136  
   7.137 -fun add_dependency loc (name, morph) mixin export thy =
   7.138 +fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   7.139    let
   7.140      val serial' = serial ();
   7.141      val thy' = thy |>
   7.142 @@ -603,7 +609,7 @@
   7.143          (registrations_of context' loc) (Idents.get context', []);
   7.144    in
   7.145      thy'
   7.146 -    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
   7.147 +    |> fold_rev (fn dep => add_registration_theory {dep = dep, mixin = NONE, export = export}) regs
   7.148    end;
   7.149  
   7.150  
     8.1 --- a/src/Pure/PIDE/command.ML	Thu Aug 30 18:40:53 2018 +0200
     8.2 +++ b/src/Pure/PIDE/command.ML	Thu Aug 30 19:59:36 2018 +0200
     8.3 @@ -70,7 +70,8 @@
     8.4      val text = File.read full_path;
     8.5      val lines = split_lines text;
     8.6      val digest = SHA1.digest text;
     8.7 -  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
     8.8 +    val file_pos = Position.copy_id pos (Path.position full_path);
     8.9 +  in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    8.10    handle ERROR msg => error (msg ^ Position.here pos);
    8.11  
    8.12  val read_file = read_file_node "";
     9.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 30 18:40:53 2018 +0200
     9.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 30 19:59:36 2018 +0200
     9.3 @@ -706,14 +706,16 @@
     9.4      def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     9.5      def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
     9.6  
     9.7 +    def lookup_id(id: Document_ID.Generic): Option[Command.State] =
     9.8 +      commands.get(id) orElse execs.get(id)
     9.9 +
    9.10      private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
    9.11        id == st.command.id ||
    9.12        (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
    9.13  
    9.14      private def other_id(id: Document_ID.Generic)
    9.15        : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] =
    9.16 -      (execs.get(id) orElse commands.get(id)).map(st =>
    9.17 -        ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
    9.18 +      lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
    9.19  
    9.20      private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
    9.21        (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
    9.22 @@ -1077,7 +1079,7 @@
    9.23          /* find command */
    9.24  
    9.25          def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
    9.26 -          state.commands.get(id) orElse state.execs.get(id) match {
    9.27 +          state.lookup_id(id) match {
    9.28              case None => None
    9.29              case Some(st) =>
    9.30                val command = st.command