# HG changeset patch
# User wenzelm
# Date 1344190292 -7200
# Node ID eeb4480b5877c22262779383a62149d23cb11209
# Parent  162579d4ba1543166abd9bab9267fb8bc47f10cb
more on isabelle mkroot;

diff -r 162579d4ba15 -r eeb4480b5877 NEWS
--- a/NEWS	Sun Aug 05 16:20:34 2012 +0200
+++ b/NEWS	Sun Aug 05 20:11:32 2012 +0200
@@ -85,6 +85,10 @@
 
   isabelle build -s -b HOLCF
 
+* The "isabelle mkroot" tool prepares session root directories for use
+with "isabelle build", similar to former "isabelle mkdir" for
+"isabelle usedir".
+
 * Discontinued support for Poly/ML 5.2.1, which was the last version
 without exception positions and advanced ML compiler/toplevel
 configuration.
diff -r 162579d4ba15 -r eeb4480b5877 doc-src/System/Thy/Sessions.thy
--- 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
diff -r 162579d4ba15 -r eeb4480b5877 doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Sun Aug 05 16:20:34 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Sun Aug 05 20:11:32 2012 +0200
@@ -402,6 +402,52 @@
 \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
diff -r 162579d4ba15 -r eeb4480b5877 lib/Tools/mkroot
--- a/lib/Tools/mkroot	Sun Aug 05 16:20:34 2012 +0200
+++ b/lib/Tools/mkroot	Sun Aug 05 20:11:32 2012 +0200
@@ -143,7 +143,7 @@
 fi
 
 cat >> "$DIR/ROOT" <<EOF
-session "$NAME" = "$ISABELLE_LOGIC" +
+session "$NAME"! = "$ISABELLE_LOGIC" +
   options [document = $ISABELLE_DOC_FORMAT]
   theories "Ex"
   files "document/root.tex"
@@ -152,19 +152,25 @@
 
 # notes
 
+if [ "$DIR" = . ]; then
+  OPT_DIR="-d."
+else
+  OPT_DIR="-d \"$DIR\""
+fi
+
 cat <<EOF
 
 Notes:
 
-  * $DIR_NAME/Ex.thy contains an example theory
+  * $DIR_NAME/Ex.thy contains an example theory.
 
-  * $DIR_NAME/document/root.tex contains the LaTeX master document setup
+  * $DIR_NAME/document/root.tex contains the LaTeX master document setup.
 
-  * $DIR/ROOT contains build options, theories and extra file dependencies
+  * $DIR/ROOT contains build options, theories and extra file dependencies.
 
-  * the following command line builds the session (with document):
+  * The following command line builds the session (with document):
 
-      isabelle build -v -d $DIR ${ISABELLE_LOGIC}-${NAME}
+      isabelle build -v $OPT_DIR $NAME
 
 EOF