src/Pure/Tools/server_commands.scala
changeset 67922 9e668ae81f97
parent 67921 1722384ffd4a
child 67923 3e072441c96a
--- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 15:11:14 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:20:53 2018 +0100
@@ -40,7 +40,7 @@
       preferences: String = default_preferences,
       options: List[String] = Nil,
       dirs: List[String] = Nil,
-      all_known: Boolean = false,
+      include_sessions: List[String] = Nil,
       system_mode: Boolean = false,
       verbose: Boolean = false)
 
@@ -50,13 +50,13 @@
         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 _)
-        all_known <- JSON.bool_default(json, "all_known")
+        include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _)
         system_mode <- JSON.bool_default(json, "system_mode")
         verbose <- JSON.bool_default(json, "verbose")
       }
       yield {
         Args(session, preferences = preferences, options = options, dirs = dirs,
-          all_known = all_known, system_mode = system_mode, verbose = verbose)
+          include_sessions = include_sessions, system_mode = system_mode, verbose = verbose)
       }
 
     def command(args: Args, progress: Progress = No_Progress)
@@ -67,7 +67,7 @@
 
       val base_info =
         Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
-          all_known = args.all_known)
+          include_sessions = args.include_sessions)
       val base = base_info.check_base
 
       val results =