# HG changeset patch
# User wenzelm
# Date 1534001580 -7200
# Node ID a6cc4302c380d16caf85b4cae46126cae7aed73a
# Parent  e90cf766723cb300e1d46b11e4e7a1a91d92ca28
tuned signature;

diff -r e90cf766723c -r a6cc4302c380 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Sat Aug 11 17:28:20 2018 +0200
+++ b/src/Pure/General/json.scala	Sat Aug 11 17:33:00 2018 +0200
@@ -376,4 +376,9 @@
     value(obj, name, Value.List.unapply(_, unapply))
   def list_default[A](obj: T, name: String, unapply: T => Option[A], default: => List[A] = Nil)
     : Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default)
+
+  def strings(obj: T, name: String): Option[List[String]] =
+    list(obj, name, JSON.Value.String.unapply _)
+  def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
+    list_default(obj, name, JSON.Value.String.unapply _, default)
 }
diff -r e90cf766723c -r a6cc4302c380 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sat Aug 11 17:28:20 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Sat Aug 11 17:33:00 2018 +0200
@@ -36,9 +36,9 @@
       for {
         session <- JSON.string(json, "session")
         preferences <- JSON.string_default(json, "preferences", default_preferences)
-        options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
-        dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
-        include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _)
+        options <- JSON.strings_default(json, "options")
+        dirs <- JSON.strings_default(json, "dirs")
+        include_sessions <- JSON.strings_default(json, "include_sessions")
         system_mode <- JSON.bool_default(json, "system_mode")
         verbose <- JSON.bool_default(json, "verbose")
       }
@@ -102,7 +102,7 @@
     def unapply(json: JSON.T): Option[Args] =
       for {
         build <- Session_Build.unapply(json)
-        print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _)
+        print_mode <- JSON.strings_default(json, "print_mode")
       }
       yield Args(build = build, print_mode = print_mode)
 
@@ -164,7 +164,7 @@
     def unapply(json: JSON.T): Option[Args] =
       for {
         session_id <- JSON.uuid(json, "session_id")
-        theories <- JSON.list(json, "theories", JSON.Value.String.unapply _)
+        theories <- JSON.strings(json, "theories")
         master_dir <- JSON.string_default(json, "master_dir")
         pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
         unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
@@ -249,7 +249,7 @@
     def unapply(json: JSON.T): Option[Args] =
       for {
         session_id <- JSON.uuid(json, "session_id")
-        theories <- JSON.list_default(json, "theories", JSON.Value.String.unapply _)
+        theories <- JSON.strings_default(json, "theories")
         master_dir <- JSON.string_default(json, "master_dir")
         all <- JSON.bool_default(json, "all")
       }