# HG changeset patch
# User wenzelm
# Date 1592662713 -7200
# Node ID 34be842f35310ccfe8692f536c374024a54412d1
# Parent  67fb92378224be1a7d611c9a81a37fc180e43ba9
share cache for parallel sessions;

diff -r 67fb92378224 -r 34be842f3531 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Jun 20 15:09:20 2020 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Jun 20 16:18:33 2020 +0200
@@ -1085,6 +1085,9 @@
   {
     override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
 
+    val xml_cache: XML.Cache = XML.make_cache()
+    val xz_cache: XZ.Cache = XZ.make_cache()
+
 
     /* directories */
 
@@ -1199,9 +1202,6 @@
 
     /* SQL database content */
 
-    val xml_cache: XML.Cache = XML.make_cache()
-    val xz_cache: XZ.Cache = XZ.make_cache()
-
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       db.using_statement(Session_Info.table.select(List(column),
         Session_Info.session_name.where_equal(name)))(stmt =>
diff -r 67fb92378224 -r 34be842f3531 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jun 20 15:09:20 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jun 20 16:18:33 2020 +0200
@@ -218,7 +218,11 @@
 
         if (options.bool("pide_session")) {
           val resources = new Resources(sessions_structure, deps(parent))
-          val session = new Session(options, resources)
+          val session =
+            new Session(options, resources) {
+              override val xml_cache: XML.Cache = store.xml_cache
+              override val xz_cache: XZ.Cache = store.xz_cache
+            }
 
           val build_session_errors: Promise[List[String]] = Future.promise
           val stdout = new StringBuilder(1000)