--- a/src/Pure/Tools/server_commands.scala Thu Mar 22 14:27:32 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Thu Mar 22 14:42:14 2018 +0100
@@ -30,10 +30,7 @@
preferences: String = default_preferences,
options: List[String] = Nil,
dirs: List[String] = Nil,
- ancestor_session: String = "",
all_known: Boolean = false,
- focus_session: Boolean = false,
- required_session: Boolean = false,
system_mode: Boolean = false,
verbose: Boolean = false)
@@ -43,17 +40,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 _)
- ancestor_session <- JSON.string_default(json, "ancestor_session")
all_known <- JSON.bool_default(json, "all_known")
- focus_session <- JSON.bool_default(json, "focus_session")
- required_session <- JSON.bool_default(json, "required_session")
system_mode <- JSON.bool_default(json, "system_mode")
verbose <- JSON.bool_default(json, "verbose")
}
yield {
Args(session, preferences = preferences, options = options, dirs = dirs,
- ancestor_session = ancestor_session, all_known = all_known, focus_session = focus_session,
- required_session = required_session, system_mode = system_mode, verbose = verbose)
+ all_known = all_known, system_mode = system_mode, verbose = verbose)
}
def command(args: Args, progress: Progress = No_Progress)
@@ -63,14 +56,8 @@
val dirs = args.dirs.map(Path.explode(_))
val base_info =
- Sessions.base_info(options,
- args.session,
- progress = progress,
- dirs = dirs,
- ancestor_session = proper_string(args.ancestor_session),
- all_known = args.all_known,
- focus_session = args.focus_session,
- required_session = args.required_session)
+ Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
+ all_known = args.all_known)
val base = base_info.check_base
val results =