# HG changeset patch
# User wenzelm
# Date 1595281529 -7200
# Node ID efb7fd4a6d1f949475b91994798b045c3a9057eb
# Parent  69880fdc8310ff306ca7a98da47ed153cc9cdbd1
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
explicitly check for extend as identity;

diff -r 69880fdc8310 -r efb7fd4a6d1f NEWS
--- 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.
diff -r 69880fdc8310 -r efb7fd4a6d1f src/Doc/Implementation/Prelim.thy
--- 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>
diff -r 69880fdc8310 -r efb7fd4a6d1f src/Pure/context.ML
--- 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;