--- a/src/Doc/System/Sessions.thy Mon Oct 14 13:21:53 2019 +0200
+++ b/src/Doc/System/Sessions.thy Mon Oct 14 17:19:08 2019 +0200
@@ -548,6 +548,7 @@
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: "dump")
+ -P split into standard partitions (AFP, non-AFP, ...)
-R operate on requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
@@ -567,9 +568,12 @@
theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close>
in the current directory).
- \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
- its theories are not processed again, and their PIDE session database is
- excluded from the dump.
+ \<^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.
+
+ \<^medskip> Option \<^verbatim>\<open>-P\<close> indicates a split into standard partitions, for improved
+ scalability of the PIDE session.
\<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
(\secref{sec:tool-build}).