doc-src/System/Thy/Sessions.thy
changeset 48683 eeb4480b5877
parent 48650 47330b712f8f
child 48684 9170e10c651e
--- a/doc-src/System/Thy/Sessions.thy	Sun Aug 05 16:20:34 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Sun Aug 05 20:11:32 2012 +0200
@@ -286,4 +286,43 @@
 \end{ttbox}
 *}
 
+
+section {* Preparing session root directories \label{sec:tool-mkroot} *}
+
+text {* The @{tool_def mkroot} tool prepares Isabelle session source
+  directories, including some @{verbatim ROOT} entry, an example
+  theory file, and some initial configuration for document preparation
+  (see also \chref{ch:present}).  The usage of @{tool 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 @{verbatim NAME} above.  The @{verbatim ROOT} file is in
+  the parent position relative to that --- it could refer to several
+  such sessions.  The @{tool mkroot} tool is conservative in the sense
+  that does not overwrite an existing session sub-directory; an
+  already existing @{verbatim ROOT} file is extended.
+
+  The implicit Isabelle settings variable @{setting ISABELLE_LOGIC}
+  specifies the parent session, and @{setting
+  ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
+  into the generated @{verbatim ROOT} file.  *}
+
+
+subsubsection {* Examples *}
+
+text {* The following produces an example session, relatively to the
+  @{verbatim ROOT} in the current directory:
+\begin{ttbox}
+isabelle mkroot Test && isabelle build -v -d. Test
+\end{ttbox}
+
+  Option @{verbatim "-v"} is not required, but useful to reveal the
+  the location of generated documents.  *}
+
 end