# HG changeset patch
# User wenzelm
# Date 1717439305 -7200
# Node ID 534c5e4f07c0b7bc1d71c9594f70b66e1f07cfc8
# Parent  07ddd501120af7f1a78b948fa8d0b866234d7ddd
minor performance tuning: more compact data;

diff -r 07ddd501120a -r 534c5e4f07c0 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Jun 03 19:43:21 2024 +0200
+++ b/src/Pure/General/table.ML	Mon Jun 03 20:28:25 2024 +0200
@@ -592,15 +592,20 @@
 (* cache *)
 
 fun unsynchronized_cache f =
-  let val cache = Unsynchronized.ref empty in
+  let
+    val cache1 = Unsynchronized.ref empty;
+    val cache2 = Unsynchronized.ref empty;
+  in
     fn x =>
-      (case lookup (! cache) x of
-        SOME result => Exn.release result
+      (case lookup (! cache1) x of
+        SOME y => y
       | NONE =>
-          let
-            val result = Exn.result f x;
-            val _ = Unsynchronized.change cache (update (x, result));
-          in Exn.release result end)
+          (case lookup (! cache2) x of
+            SOME exn => Exn.reraise exn
+          | NONE =>
+              (case Exn.result f x of
+                Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
+              | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))))
   end;