clarified signature: do not expose somewhat accidental internal options;

--- a/src/Doc/System/Server.thy	Thu Mar 22 14:27:32 2018 +0100
+++ b/src/Doc/System/Server.thy	Thu Mar 22 14:42:14 2018 +0100
@@ -627,13 +627,12 @@
   \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
   \quad~~\<open>options?: [string],\<close> \\
   \quad~~\<open>dirs?: [string],\<close> \\
-  \quad~~\<open>ancestor_session?: string,\<close> \\
   \quad~~\<open>all_known?: bool,\<close> \\
-  \quad~~\<open>focus_session?: bool,\<close> \\
-  \quad~~\<open>required_session?: bool,\<close> \\
   \quad~~\<open>system_mode?: bool,\<close> \\
   \quad~~\<open>verbose?: bool}\<close> \\[2ex]
+  \end{tabular}
 
+  \begin{tabular}{ll}
   \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
   \quad\<open>{session: string,\<close> \\
   \quad~~\<open>ok: bool,\<close> \\
@@ -669,10 +668,9 @@
 subsubsection \<open>Arguments\<close>
 
 text \<open>
-  The \<open>session\<close> field is mandatory. It specifies the target session name:
-  either directly (default) or indirectly (if \<open>required_session\<close> is \<^verbatim>\<open>true\<close>).
-  The build process will produce all required ancestor images for the
-  specified target.
+  The \<open>session\<close> field specifies the target session name. The build process
+  will produce all required ancestor images according to the overall session
+  graph.
 
   \<^medskip>
   The environment of Isabelle system options is determined from \<open>preferences\<close>
@@ -691,13 +689,6 @@
   sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
 
   \<^medskip>
-  The \<open>ancestor_session\<close> field specifies an alternative image as starting
-  point for the target image. The default is to use the parent session
-  according to the ROOT entry; see also option \<^verbatim>\<open>-A\<close> in @{tool jedit}. This
-  can lead to a more light-weight build process, by skipping intermediate
-  session images of the hierarchy that are not used later on.
-
-  \<^medskip>
   The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all sessions from reachable
   ROOT entries into the name space of theories. This is relevant for proper
   session-qualified names, instead of referring to theory file names. The
@@ -707,17 +698,6 @@
   session directories and theory dependencies.
 
   \<^medskip>
-  The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> focuses on the target session:
-  the accessible name space of theories is restricted to sessions that are
-  connected to it in the imports graph.
-
-  \<^medskip>
-  The \<open>required_session\<close> field set to \<^verbatim>\<open>true\<close> indicates that the target image
-  should not be the \<open>session\<close>, but its parent (or ancestor according to
-  \<open>ancestor_session\<close>). Thus it prepares a session context where theories from
-  the \<open>session\<close> itself can be loaded.
-
-  \<^medskip>
   The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
   log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
@@ -771,9 +751,6 @@
 
   Build a session image from the Archive of Formal Proofs:
   @{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
-
-  Build of a session image of \<^verbatim>\<open>HOL-Number_Theory\<close> directly on top of \<^verbatim>\<open>HOL\<close>:
-  @{verbatim [display] \<open>session_build {"session": "HOL-Number_Theory", "ancestor_session": "HOL"}\<close>}
 \<close>
 
 

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