# HG changeset patch
# User wenzelm
# Date 1562236284 -7200
# Node ID 34b271c4f400e07606ca3a6bad5178f55642686b
# Parent  03430649a7d287b4f3a4872035d51897acbcadbe
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;

diff -r 03430649a7d2 -r 34b271c4f400 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Jul 04 11:26:00 2019 +0200
+++ b/src/Pure/context.ML	Thu Jul 04 12:31:24 2019 +0200
@@ -50,6 +50,7 @@
   val subthy: theory * theory -> bool
   val trace_theories: bool Unsynchronized.ref
   val theories_trace: unit -> {active_positions: Position.T list, active: int, total: int}
+  val join_thys: theory * theory -> theory
   val begin_thy: string -> theory list -> theory
   val finish_thy: theory -> theory
   val theory_data_size: theory -> (Position.T * int) list
@@ -365,7 +366,39 @@
 end;
 
 
-(* named theory nodes *)
+(* join: anonymous theory nodes *)
+
+local
+
+fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]);
+
+fun join_history thys =
+  apply2 history_of thys |>
+  (fn ({name, stage}, {name = name', stage = stage'}) =>
+    if name = name' andalso is_some stage andalso is_some stage' then
+      {name = name, stage = Option.map next_stage stage}
+    else bad_join thys);
+
+fun join_ancestry thys =
+  apply2 ancestry_of thys |>
+  (fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
+    if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors')
+    then ancestry else bad_join thys);
+
+in
+
+fun join_thys thys =
+  let
+    val ids = merge_ids thys;
+    val history = join_history thys;
+    val ancestry = join_ancestry thys;
+    val data = merge_data thys (apply2 data_of thys);
+  in create_thy ids history ancestry data end;
+
+end;
+
+
+(* merge: named theory nodes *)
 
 local
 
diff -r 03430649a7d2 -r 34b271c4f400 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Jul 04 11:26:00 2019 +0200
+++ b/src/Pure/theory.ML	Thu Jul 04 12:31:24 2019 +0200
@@ -23,6 +23,7 @@
   val defs_of: theory -> Defs.T
   val at_begin: (theory -> theory option) -> theory -> theory
   val at_end: (theory -> theory option) -> theory -> theory
+  val join_theory: theory list -> theory
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
@@ -168,6 +169,11 @@
 val defs_of = #defs o rep_theory;
 
 
+(* join theory *)
+
+val join_theory = foldl1 Context.join_thys;
+
+
 (* begin/end theory *)
 
 val begin_wrappers = rev o #1 o #wrappers o rep_theory;