diff -r 1722384ffd4a -r 9e668ae81f97 src/Pure/Tools/server_commands.scala --- 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 =