doc-src/System/Thy/document/Sessions.tex

 isabelle build -a -n -c
 \end{ttbox}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Preparing session root directories \label{sec:tool-mkroot}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{mkroot}\hypertarget{tool.mkroot}{\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}}} tool prepares Isabelle session source
+  directories, including some \verb|ROOT| entry, an example
+  theory file, and some initial configuration for document preparation
+  (see also \chref{ch:present}).  The usage of \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} is:
+
+\begin{ttbox}
+Usage: isabelle mkroot NAME
+
+  Prepare session root directory, adding session NAME with
+  built-in document preparation.
+\end{ttbox}
+
+  All session-specific files are placed into a separate sub-directory
+  given as \verb|NAME| above.  The \verb|ROOT| file is in
+  the parent position relative to that --- it could refer to several
+  such sessions.  The \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} tool is conservative in the sense
+  that does not overwrite an existing session sub-directory; an
+  already existing \verb|ROOT| file is extended.
+
+  The implicit Isabelle settings variable \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}}
+  specifies the parent session, and \hyperlink{setting.ISABELLE-DOCUMENT-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCUMENT{\isaliteral{5F}{\isacharunderscore}}FORMAT}}}} the document format to be filled filled
+  into the generated \verb|ROOT| file.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The following produces an example session, relatively to the
+  \verb|ROOT| in the current directory:
+\begin{ttbox}
+isabelle mkroot Test && isabelle build -v -d. Test
+\end{ttbox}
+
+  Option \verb|-v| is not required, but useful to reveal the
+  the location of generated documents.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory