src/Doc/System/Server.thy

   \<^bold>\<open>type\<close> \<open>session_build_args =\<close> \\
   \quad\<open>{session: string,\<close> \\
   \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
   \quad~~\<open>options?: [string],\<close> \\
   \quad~~\<open>dirs?: [string],\<close> \\
-  \quad~~\<open>all_known?: bool,\<close> \\
+  \quad~~\<open>include_sessions: [string],\<close> \\
   \quad~~\<open>system_mode?: bool,\<close> \\
   \quad~~\<open>verbose?: bool}\<close> \\[2ex]
   \end{tabular}
 
   \begin{tabular}{ll}

   The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
   files (\secref{sec:session-root}). This augments the name space of available
   sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
 
   \<^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
-  option enables the \<^verbatim>\<open>use_theories\<close> command
-  (\secref{sec:command-use-theories}) to refer to arbitrary theories from
-  other sessions, but considerable time is required to explore all accessible
-  session directories and theory dependencies.
+  The \<open>include_sessions\<close> field specifies sessions whose theories should be
+  included in the overall name space of session-qualified theory names. This
+  corresponds to a \<^bold>\<open>sessions\<close> specification in ROOT files
+  (\secref{sec:session-root}). It enables the \<^verbatim>\<open>use_theories\<close> command
+  (\secref{sec:command-use-theories}) to refer to sources from other sessions
+  in a robust manner, instead of relying on directory locations.
 
   \<^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

   context of an already started session for Isabelle/HOL (see also
   \secref{sec:command-session-start}):
   @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Isar_Examples/Drinker"]}\<close>}
 
   \<^medskip>
-  Process some example theories that import other theories via
-  session-qualified theory names:
-
-  @{verbatim [display] \<open>session_start {"session": "HOL", "all_known": true}
-use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
-session_stop {"session_id": ...}\<close>}
-
-  The option \<open>all_known\<close> has been used here to the full name space of
-  session-qualified theory names accessible in this session. This is also the
-  default in Isabelle/jEdit, although it requires significant startup time.
-
-  \<^medskip>
   Process some example theories in the context of their (single) parent
   session:
 
   @{verbatim [display] \<open>session_start {"session": "HOL-Library"}
 use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
 session_stop {"session_id": ...}\<close>}
+
+  \<^medskip>
+  Process some example theories that import other theories via
+  session-qualified theory names:
+
+  @{verbatim [display] \<open>session_start {"session": "HOL", "include_sessions": ["HOL-Unix"]}
+use_theories {"session_id": ..., "theories": ["HOL-Unix.Unix"]}
+session_stop {"session_id": ...}\<close>}
 \<close>
 
 end