# HG changeset patch
# User wenzelm
# Date 1637165517 -3600
# Node ID 1e7bb95c75e73d07726d77f0bb8160ca566276c5
# Parent  cfc15da73a78a34ea7de234a05ffc1add17fa0f2
more parallelism, at the cost of potential duplicates of make_thy;

diff -r cfc15da73a78 -r 1e7bb95c75e7 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 17 15:54:11 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 17 17:11:57 2021 +0100
@@ -75,15 +75,18 @@
     private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
     def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
     {
-      theory_cache.change_result(thys =>
-      {
-        thys.get(thy_name) match {
-          case Some(thy) => (thy, thys)
-          case None =>
-            val thy = make_thy
-            (thy, thys + (thy_name -> thy))
-        }
-      })
+      theory_cache.value.get(thy_name) match {
+        case Some(thy) => thy
+        case None =>
+          val thy1 = make_thy
+          theory_cache.change_result(thys =>
+          {
+            thys.get(thy_name) match {
+              case Some(thy) => (thy, thys)
+              case None => (thy1, thys + (thy_name -> thy1))
+            }
+          })
+      }
     }
   }