--- 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 =