src/Pure/Tools/server_commands.scala
changeset 67919 dd90faed43b2
parent 67916 a72f01c63262
child 67920 c3c74310154e
--- 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 =