# HG changeset patch
# User wenzelm
# Date 1571074632 -7200
# Node ID a4ccd277e9c49158748369f1a9639e36ef9fa155
# Parent  cb07f21c99167c77dac42c7470e50ff2d8801038
clarified treatment of base logic image;

diff -r cb07f21c9916 -r a4ccd277e9c4 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Oct 14 19:14:03 2019 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Oct 14 19:37:12 2019 +0200
@@ -551,9 +551,9 @@
     -R           operate on requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
+    -b NAME      base logic image (default "Pure")
     -d DIR       include session directory
     -g NAME      select session group NAME
-    -l NAME      logic session name (default "Pure")
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
@@ -568,8 +568,8 @@
   in the current directory).
 
   \<^medskip> Option \<^verbatim>\<open>-b\<close> specifies an optional base logic image, for improved
-  scalability of the PIDE session. Its theories are processed separately,
-  always starting from the \<^emph>\<open>Pure\<close> session.
+  scalability of the PIDE session. Its theories are only processed if it is
+  included in the overall session selection.
 
   \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
   (\secref{sec:tool-build}).
@@ -592,14 +592,14 @@
   @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
 
   \<^smallskip>
-  Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
-  as starting point:
-  @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
+  Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, with full bootstrap
+  from Isabelle/Pure:
+  @{verbatim [display] \<open>isabelle dump -v HOL-Analysis\<close>}
 
   \<^smallskip>
-  Dump all sessions connected to HOL-Analysis, including a full bootstrap of
-  Isabelle/HOL from Isabelle/Pure:
-  @{verbatim [display] \<open>isabelle dump -v -l Pure -B HOL-Analysis\<close>}
+  Dump all sessions connected to HOL-Analysis, using main Isabelle/HOL as
+  basis:
+  @{verbatim [display] \<open>isabelle dump -v -b HOL -B HOL-Analysis\<close>}
 
   This results in uniform PIDE markup for everything, except for the
   Isabelle/Pure bootstrap process itself. Producing that on the spot requires
diff -r cb07f21c9916 -r a4ccd277e9c4 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Oct 14 19:14:03 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Oct 14 19:37:12 2019 +0200
@@ -152,10 +152,11 @@
         (for (name <- afp_sessions.iterator if deps.sessions_structure(name).is_afp_bulky)
           yield name).toList
 
-      val base_sessions = session_graph.all_preds(List(logic)).reverse
+      val base_sessions =
+        session_graph.all_preds(List(logic).filter(session_graph.defined)).reverse
 
       val base =
-        if (logic == isabelle.Thy_Header.PURE) Nil
+        if (logic == isabelle.Thy_Header.PURE || base_sessions.isEmpty) Nil
         else List(new Session(context, isabelle.Thy_Header.PURE, log, base_sessions))
 
       val main =
@@ -169,7 +170,7 @@
           val (part1, part2) =
           {
             val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions)
-            val force_partition1 = AFP.force_partition1.filter(graph.defined(_))
+            val force_partition1 = AFP.force_partition1.filter(graph.defined)
             val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet
             graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
           }