clarified signature: prefer selective include_sessions;

--- a/src/Doc/System/Server.thy	Thu Mar 22 15:11:14 2018 +0100
+++ b/src/Doc/System/Server.thy	Thu Mar 22 16:20:53 2018 +0100
@@ -632,7 +632,7 @@
   \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}
@@ -694,13 +694,12 @@
   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
@@ -989,24 +988,20 @@
   @{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

--- a/src/Pure/Thy/sessions.scala	Thu Mar 22 15:11:14 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 22 16:20:53 2018 +0100
@@ -373,6 +373,7 @@
     session: String,
     progress: Progress = No_Progress,
     dirs: List[Path] = Nil,
+    include_sessions: List[String] = Nil,
     ancestor_session: Option[String] = None,
     all_known: Boolean = false,
     focus_session: Boolean = false,
@@ -435,15 +436,17 @@
       if (infos1.isEmpty) full_sessions
       else load_structure(options, dirs = dirs, infos = infos1)
 
-    val select_sessions1 =
-      if (focus_session) full_sessions1.imports_descendants(List(session1))
-      else List(session1)
     val selected_sessions1 =
+    {
+      val sel_sessions1 = session1 :: include_sessions
+      val select_sessions1 =
+        if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
       full_sessions1.selection(Selection(sessions = select_sessions1))
+    }
 
     val sessions1 = if (all_known) full_sessions1 else selected_sessions1
     val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
-    val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
+    val base1 = deps1(session1).copy(known = deps1.all_known)
 
     Base_Info(options, dirs, session1, sessions1, deps1.errors, base1, infos1)
   }

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