changeset 67827 | b027c97c77c9 |
parent 67818 | 2457bea123e4 |
child 68169 | 395432e7516e |
--- 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))