--- a/src/Doc/System/Sessions.thy Fri Feb 15 12:34:29 2019 +0100
+++ b/src/Doc/System/Sessions.thy Fri Feb 15 17:00:21 2019 +0100
@@ -145,13 +145,14 @@
\<^verbatim>\<open>document\<close> within the session root directory.
\<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number]
- patterns\<close> writes theory exports to the file-system: the \<open>target_dir\<close>
- specification is relative to the session root directory; its default is
- \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref export}
- (\secref{sec:tool-export}). The number given in brackets (default: 0)
- specifies elements that should be pruned from each name: it allows to reduce
- the resulting directory hierarchy at the danger of overwriting files due to
- loss of uniqueness.
+ patterns\<close> specifies theory exports that may get written to the file-system,
+ e.g. via @{tool_ref build} with option \<^verbatim>\<open>-e\<close> (\secref{sec:tool-build}). The
+ \<open>target_dir\<close> specification is relative to the session root directory; its
+ default is \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref
+ export} (\secref{sec:tool-export}). The number given in brackets (default:
+ 0) specifies elements that should be pruned from each name: it allows to
+ reduce the resulting directory hierarchy at the danger of overwriting files
+ due to loss of uniqueness.
\<close>
@@ -288,6 +289,7 @@
-b build heap images
-c clean build
-d DIR include session directory
+ -e export files from session specification into file-system
-f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
@@ -374,6 +376,15 @@
parent or import graph) before performing the specified build operation.
\<^medskip>
+ Option \<^verbatim>\<open>-e\<close> executes the \isakeyword{export_files} directives from the ROOT
+ specification of all explicitly selected sessions: the status of the session
+ build database needs to be OK, but the session could have been built
+ earlier. Using \isakeyword{export_files}, a session may serve as abstract
+ interface for add-on build artefacts, but these are only materialized on
+ explicit request: without option \<^verbatim>\<open>-e\<close> there is no effect on the physical
+ file-system yet.
+
+ \<^medskip>
Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
requirements.