more permissive string fields;

--- a/src/Pure/General/json.scala	Wed Dec 18 10:39:38 2019 +0100
+++ b/src/Pure/General/json.scala	Wed Dec 18 15:10:13 2019 +0100
@@ -260,6 +260,16 @@
         }
     }
 
+    object String0
+    {
+      def unapply(json: T): Option[java.lang.String] =
+        json match {
+          case null => Some("")
+          case x: java.lang.String => Some(x)
+          case _ => None
+        }
+    }
+
     object Double
     {
       def unapply(json: T): Option[scala.Double] =
@@ -361,6 +371,11 @@
   def string_default(obj: T, name: String, default: => String = ""): Option[String] =
     value_default(obj, name, Value.String.unapply, default)
 
+  def string0(obj: T, name: String): Option[String] =
+    value(obj, name, Value.String0.unapply)
+  def string0_default(obj: T, name: String, default: => String = ""): Option[String] =
+    value_default(obj, name, Value.String0.unapply, default)
+
   def double(obj: T, name: String): Option[Double] =
     value(obj, name, Value.Double.unapply)
   def double_default(obj: T, name: String, default: => Double = 0.0): Option[Double] =