src/Pure/General/json.scala
author wenzelm
Tue, 09 Aug 2016 23:18:42 +0200
changeset 63644 ed266398da33
child 63992 3aa9837d05c7
permissions -rw-r--r--
support for JSON parsing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63644
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/json.scala
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     3
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     4
Support for JSON parsing.
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     5
*/
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     6
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     7
package isabelle
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     8
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
     9
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    10
object JSON
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    11
{
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    12
  /* parse */
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    13
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    14
  def parse(text: String): Any =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    15
    scala.util.parsing.json.JSON.parseFull(text) getOrElse error("Malformed JSON")
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    16
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    17
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    18
  /* field access */
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    19
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    20
  def any(obj: Any, name: String): Option[Any] =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    21
    obj match {
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    22
      case m: Map[String, Any] => m.get(name)
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    23
      case _ => None
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    24
    }
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    25
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    26
  def array(obj: Any, name: String): List[Any] =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    27
    any(obj, name) match {
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    28
      case Some(a: List[Any]) => a
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    29
      case _ => Nil
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    30
    }
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    31
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    32
  def string(obj: Any, name: String): Option[String] =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    33
    any(obj, name) match {
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    34
      case Some(x: String) => Some(x)
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    35
      case _ => None
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    36
    }
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    37
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    38
  def double(obj: Any, name: String): Option[Double] =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    39
    any(obj, name) match {
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    40
      case Some(x: Double) => Some(x)
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    41
      case _ => None
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    42
    }
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    43
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    44
  def long(obj: Any, name: String): Option[Long] =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    45
    double(obj, name).map(_.toLong)
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    46
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    47
  def int(obj: Any, name: String): Option[Int] =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    48
    double(obj, name).map(_.toInt)
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    49
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    50
  def bool(obj: Any, name: String): Option[Boolean] =
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    51
    any(obj, name) match {
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    52
      case Some(x: Boolean) => Some(x)
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    53
      case _ => None
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    54
    }
ed266398da33 support for JSON parsing;
wenzelm
parents:
diff changeset
    55
}