--- 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.
--- 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
--- 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
--- 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