# 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