tuned;

--- 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))