# HG changeset patch
# User wenzelm
# Date 1520798927 -3600
# Node ID b027c97c77c92ab755ed490357a4cbf82c9119c4
# Parent  5ea76b219668b9235b326f422908b72d84e20777
tuned;

diff -r 5ea76b219668 -r b027c97c77c9 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun Mar 11 20:56:42 2018 +0100
+++ b/src/Pure/PIDE/xml.scala	Sun Mar 11 21:08:47 2018 +0100
@@ -178,7 +178,8 @@
     }
 
     private def cache_string(x: String): String =
-      if (x == "true") "true"
+      if (x == "") ""
+      else if (x == "true") "true"
       else if (x == "false") "false"
       else if (x == "0.0") "0.0"
       else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))