separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
authorwenzelm
Fri Oct 27 15:49:09 2017 +0200 (19 months ago)
changeset 669258b117dc73278
parent 66924 b4d4027f743b
child 66926 4cf560a6dd84
separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;
src/Pure/General/json.scala
     1.1 --- a/src/Pure/General/json.scala	Fri Oct 27 13:50:08 2017 +0200
     1.2 +++ b/src/Pure/General/json.scala	Fri Oct 27 15:49:09 2017 +0200
     1.3 @@ -7,9 +7,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.util.parsing.combinator.Parsers
     1.8  import scala.util.parsing.combinator.lexical.Scanners
     1.9  import scala.util.parsing.input.CharArrayReader.EofCh
    1.10 -import scala.util.parsing.json.{JSONObject, JSONArray}
    1.11  
    1.12  
    1.13  object JSON
    1.14 @@ -28,6 +28,7 @@
    1.15    sealed case class Token(kind: Kind.Value, text: String)
    1.16    {
    1.17      def is_keyword: Boolean = kind == Kind.KEYWORD
    1.18 +    def is_keyword(name: String): Boolean = kind == Kind.KEYWORD && text == name
    1.19      def is_string: Boolean = kind == Kind.STRING
    1.20      def is_number: Boolean = kind == Kind.NUMBER
    1.21      def is_error: Boolean = kind == Kind.ERROR
    1.22 @@ -105,14 +106,49 @@
    1.23    }
    1.24  
    1.25  
    1.26 +  /* parser */
    1.27 +
    1.28 +  trait Parser extends Parsers
    1.29 +  {
    1.30 +    type Elem = Token
    1.31 +
    1.32 +    def $$$(name: String): Parser[Token] = elem(name, _.is_keyword(name))
    1.33 +    def string: Parser[String] = elem("string", _.is_string) ^^ (_.text)
    1.34 +    def number: Parser[Double] = elem("number", _.is_number) ^^ (tok => tok.text.toDouble)
    1.35 +
    1.36 +    def json_object: Parser[Map[String, T]] =
    1.37 +      $$$("{") ~>
    1.38 +        repsep(string ~ ($$$(":") ~> json_value) ^^ { case a ~ b => (a, b) }, $$$(",")) <~
    1.39 +      $$$("}") ^^ (_.toMap)
    1.40 +
    1.41 +    def json_array: Parser[List[T]] =
    1.42 +      $$$("[") ~> repsep(json_value, $$$(",")) <~ $$$("]")
    1.43 +
    1.44 +    def json_value: Parser[T] =
    1.45 +      json_object | (json_array | (number | (string |
    1.46 +        ($$$("true") ^^^ true | ($$$("false") ^^^ false | ($$$("null") ^^^ null))))))
    1.47 +
    1.48 +    def parse(input: CharSequence, strict: Boolean): T =
    1.49 +    {
    1.50 +      val scanner = new Lexer.Scanner(Scan.char_reader(input))
    1.51 +      phrase(if (strict) json_object | json_array else json_value)(scanner) match {
    1.52 +        case Success(json, _) => json
    1.53 +        case NoSuccess(_, next) => error("Malformed JSON input at " + next.pos)
    1.54 +      }
    1.55 +    }
    1.56 +  }
    1.57 +
    1.58 +  object Parser extends Parser
    1.59 +
    1.60 +
    1.61    /* standard format */
    1.62  
    1.63 -  def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON")
    1.64 +  def parse(s: S, strict: Boolean = true): T = Parser.parse(s, strict)
    1.65  
    1.66    object Format
    1.67    {
    1.68      def unapply(s: S): Option[T] =
    1.69 -      try { scala.util.parsing.json.JSON.parseFull(s) }
    1.70 +      try { Some(parse(s, strict = false)) }
    1.71        catch { case ERROR(_) => None }
    1.72  
    1.73      def apply(json: T): S =
    1.74 @@ -170,10 +206,8 @@
    1.75              val i = n.toLong
    1.76              result ++= (if (i.toDouble == n) i.toString else n.toString)
    1.77            case s: String => string(s)
    1.78 -          case JSONObject(obj) => object_(obj)
    1.79            case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) =>
    1.80              object_(obj.asInstanceOf[Map[String, T]])
    1.81 -          case JSONArray(list) => array(list)
    1.82            case list: List[T] => array(list)
    1.83            case _ => error("Bad JSON value: " + x.toString)
    1.84          }