src/Pure/Tools/server_commands.scala

 
     def unapply(json: JSON.T): Option[Args] =
       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")
       }
       yield {
         Args(session, preferences = preferences, options = options, dirs = dirs,

       print_mode: List[String] = Nil)
 
     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)
 
     def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
       : (JSON.Object.T, (UUID, Thy_Resources.Session)) =

       check_limit: Int = 0)
 
     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")
         export_pattern <- JSON.string_default(json, "export_pattern")
         check_delay <-

       all: Boolean = false)
 
     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")
       }
       yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }