tuned signature;
authorwenzelm
Sat Aug 11 17:33:00 2018 +0200 (6 days ago)
changeset 68742a6cc4302c380
parent 68741 e90cf766723c
child 68744 64fb127e33f7
tuned signature;
src/Pure/General/json.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/General/json.scala	Sat Aug 11 17:28:20 2018 +0200
     1.2 +++ b/src/Pure/General/json.scala	Sat Aug 11 17:33:00 2018 +0200
     1.3 @@ -376,4 +376,9 @@
     1.4      value(obj, name, Value.List.unapply(_, unapply))
     1.5    def list_default[A](obj: T, name: String, unapply: T => Option[A], default: => List[A] = Nil)
     1.6      : Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default)
     1.7 +
     1.8 +  def strings(obj: T, name: String): Option[List[String]] =
     1.9 +    list(obj, name, JSON.Value.String.unapply _)
    1.10 +  def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
    1.11 +    list_default(obj, name, JSON.Value.String.unapply _, default)
    1.12  }
     2.1 --- a/src/Pure/Tools/server_commands.scala	Sat Aug 11 17:28:20 2018 +0200
     2.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Aug 11 17:33:00 2018 +0200
     2.3 @@ -36,9 +36,9 @@
     2.4        for {
     2.5          session <- JSON.string(json, "session")
     2.6          preferences <- JSON.string_default(json, "preferences", default_preferences)
     2.7 -        options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
     2.8 -        dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
     2.9 -        include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _)
    2.10 +        options <- JSON.strings_default(json, "options")
    2.11 +        dirs <- JSON.strings_default(json, "dirs")
    2.12 +        include_sessions <- JSON.strings_default(json, "include_sessions")
    2.13          system_mode <- JSON.bool_default(json, "system_mode")
    2.14          verbose <- JSON.bool_default(json, "verbose")
    2.15        }
    2.16 @@ -102,7 +102,7 @@
    2.17      def unapply(json: JSON.T): Option[Args] =
    2.18        for {
    2.19          build <- Session_Build.unapply(json)
    2.20 -        print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _)
    2.21 +        print_mode <- JSON.strings_default(json, "print_mode")
    2.22        }
    2.23        yield Args(build = build, print_mode = print_mode)
    2.24  
    2.25 @@ -164,7 +164,7 @@
    2.26      def unapply(json: JSON.T): Option[Args] =
    2.27        for {
    2.28          session_id <- JSON.uuid(json, "session_id")
    2.29 -        theories <- JSON.list(json, "theories", JSON.Value.String.unapply _)
    2.30 +        theories <- JSON.strings(json, "theories")
    2.31          master_dir <- JSON.string_default(json, "master_dir")
    2.32          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    2.33          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    2.34 @@ -249,7 +249,7 @@
    2.35      def unapply(json: JSON.T): Option[Args] =
    2.36        for {
    2.37          session_id <- JSON.uuid(json, "session_id")
    2.38 -        theories <- JSON.list_default(json, "theories", JSON.Value.String.unapply _)
    2.39 +        theories <- JSON.strings_default(json, "theories")
    2.40          master_dir <- JSON.string_default(json, "master_dir")
    2.41          all <- JSON.bool_default(json, "all")
    2.42        }