subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
explicitly check for extend as identity;
--- a/NEWS Fri Jul 17 20:35:43 2020 +0200
+++ b/NEWS Mon Jul 20 23:45:29 2020 +0200
@@ -109,6 +109,12 @@
*** ML ***
+* Theory_Data extend operation is obsolete and needs to be the identity
+function; merge should be conservative and not reset to the empty value.
+Subtle INCOMPATIBILITY and change of semantics (due to
+Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
+the begin of a new theory can be achieved via Theory.at_begin.
+
* Antiquotations @{scala_function} and @{scala} refer to registered
Isabelle/Scala functions (of type String => String): invocation works
via the PIDE protocol.
--- a/src/Doc/Implementation/Prelim.thy Fri Jul 17 20:35:43 2020 +0200
+++ b/src/Doc/Implementation/Prelim.thy Mon Jul 20 23:45:29 2020 +0200
@@ -269,23 +269,27 @@
\begin{tabular}{ll}
\<open>\<type> T\<close> & representing type \\
\<open>\<val> empty: T\<close> & empty default value \\
- \<open>\<val> extend: T \<rightarrow> T\<close> & re-initialize on import \\
- \<open>\<val> merge: T \<times> T \<rightarrow> T\<close> & join on import \\
+ \<open>\<val> extend: T \<rightarrow> T\<close> & obsolete (identity function) \\
+ \<open>\<val> merge: T \<times> T \<rightarrow> T\<close> & merge data \\
\end{tabular}
\<^medskip>
The \<open>empty\<close> value acts as initial default for \<^emph>\<open>any\<close> theory that does not
- declare actual data content; \<open>extend\<close> acts like a unitary version of
- \<open>merge\<close>.
+ declare actual data content; \<open>extend\<close> is obsolete: it needs to be the
+ identity function.
- Implementing \<open>merge\<close> can be tricky. The general idea is that \<open>merge (data\<^sub>1,
- data\<^sub>2)\<close> inserts those parts of \<open>data\<^sub>2\<close> into \<open>data\<^sub>1\<close> that are not yet
- present, while keeping the general order of things. The \<^ML>\<open>Library.merge\<close>
- function on plain lists may serve as canonical template.
+ The \<open>merge\<close> operation needs to join the data from two theories in a
+ conservative manner. The standard scheme for \<open>merge (data\<^sub>1, data\<^sub>2)\<close>
+ inserts those parts of \<open>data\<^sub>2\<close> into \<open>data\<^sub>1\<close> that are not yet present,
+ while keeping the general order of things. The \<^ML>\<open>Library.merge\<close>
+ function on plain lists may serve as canonical template. Particularly note
+ that shared parts of the data must not be duplicated by naive concatenation,
+ or a theory graph that resembles a chain of diamonds would cause an
+ exponential blowup!
- Particularly note that shared parts of the data must not be duplicated by
- naive concatenation, or a theory graph that is like a chain of diamonds
- would cause an exponential blowup!
+ Sometimes, the data consists of a single item that cannot be ``merged'' in a
+ sensible manner. Then the standard scheme degenerates to the projection to
+ \<open>data\<^sub>1\<close>, ignoring \<open>data\<^sub>2\<close> outright.
\<close>
paragraph \<open>Proof context data\<close>
--- a/src/Pure/context.ML Fri Jul 17 20:35:43 2020 +0200
+++ b/src/Pure/context.ML Mon Jul 20 23:45:29 2020 +0200
@@ -665,11 +665,19 @@
exception Data of T;
val kind =
- Context.Theory_Data.declare
- (Position.thread_data ())
- (Data Data.empty)
- (fn Data x => Data (Data.extend x))
- (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)));
+ let val pos = Position.thread_data () in
+ Context.Theory_Data.declare
+ pos
+ (Data Data.empty)
+ (fn Data x =>
+ let
+ val y = Data.extend x;
+ val _ =
+ if pointer_eq (x, y) then ()
+ else raise Fail ("Theory_Data extend needs to be identity" ^ Position.here pos)
+ in Data y end)
+ (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)))
+ end;
val get = Context.Theory_Data.get kind (fn Data x => x);
val put = Context.Theory_Data.put kind Data;