# HG changeset patch
# User wenzelm
# Date 1470777522 -7200
# Node ID ed266398da33b0f9e778680f6db55c13660048cf
# Parent  d83a1eeff9d2b4293747e35a22c8adc88c8d5e5a
support for JSON parsing;

diff -r d83a1eeff9d2 -r ed266398da33 src/Pure/General/json.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/json.scala	Tue Aug 09 23:18:42 2016 +0200
@@ -0,0 +1,55 @@
+/*  Title:      Pure/Tools/json.scala
+    Author:     Makarius
+
+Support for JSON parsing.
+*/
+
+package isabelle
+
+
+object JSON
+{
+  /* parse */
+
+  def parse(text: String): Any =
+    scala.util.parsing.json.JSON.parseFull(text) getOrElse error("Malformed JSON")
+
+
+  /* field access */
+
+  def any(obj: Any, name: String): Option[Any] =
+    obj match {
+      case m: Map[String, Any] => m.get(name)
+      case _ => None
+    }
+
+  def array(obj: Any, name: String): List[Any] =
+    any(obj, name) match {
+      case Some(a: List[Any]) => a
+      case _ => Nil
+    }
+
+  def string(obj: Any, name: String): Option[String] =
+    any(obj, name) match {
+      case Some(x: String) => Some(x)
+      case _ => None
+    }
+
+  def double(obj: Any, name: String): Option[Double] =
+    any(obj, name) match {
+      case Some(x: Double) => Some(x)
+      case _ => None
+    }
+
+  def long(obj: Any, name: String): Option[Long] =
+    double(obj, name).map(_.toLong)
+
+  def int(obj: Any, name: String): Option[Int] =
+    double(obj, name).map(_.toInt)
+
+  def bool(obj: Any, name: String): Option[Boolean] =
+    any(obj, name) match {
+      case Some(x: Boolean) => Some(x)
+      case _ => None
+    }
+}
diff -r d83a1eeff9d2 -r ed266398da33 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Aug 09 20:35:21 2016 +0200
+++ b/src/Pure/build-jars	Tue Aug 09 23:18:42 2016 +0200
@@ -32,6 +32,7 @@
   General/graph.scala
   General/graph_display.scala
   General/graphics_file.scala
+  General/json.scala
   General/linear_set.scala
   General/long_name.scala
   General/multi_map.scala