# HG changeset patch
# User wenzelm
# Date 1609600372 -3600
# Node ID 000bcf2524fde0a1023ec900fb81296c4202ad7d
# Parent  237bd6318cc1ee5a158b0fe7f35dc1520952518b
clarified boundary case;

diff -r 237bd6318cc1 -r 000bcf2524fd src/Pure/General/cache.scala
--- a/src/Pure/General/cache.scala	Sat Jan 02 16:09:45 2021 +0100
+++ b/src/Pure/General/cache.scala	Sat Jan 02 16:12:52 2021 +0100
@@ -45,7 +45,7 @@
 
   protected def store[A](x: A): A =
   {
-    if (table == null) x
+    if (table == null || x == null) x
     else {
       table.put(x, new WeakReference[Any](x))
       x
@@ -54,7 +54,8 @@
 
   protected def cache_string(x: String): String =
   {
-    if (x == "") ""
+    if (x == null) null
+    else if (x == "") ""
     else if (x == "true") "true"
     else if (x == "false") "false"
     else if (x == "0.0") "0.0"