more on isabelle mkroot;
authorwenzelm
Sun Aug 05 20:11:32 2012 +0200 (2012-08-05)
changeset 48683eeb4480b5877
parent 48682 162579d4ba15
child 48684 9170e10c651e
more on isabelle mkroot;
NEWS
doc-src/System/Thy/Sessions.thy
doc-src/System/Thy/document/Sessions.tex
lib/Tools/mkroot
     1.1 --- a/NEWS	Sun Aug 05 16:20:34 2012 +0200
     1.2 +++ b/NEWS	Sun Aug 05 20:11:32 2012 +0200
     1.3 @@ -85,6 +85,10 @@
     1.4  
     1.5    isabelle build -s -b HOLCF
     1.6  
     1.7 +* The "isabelle mkroot" tool prepares session root directories for use
     1.8 +with "isabelle build", similar to former "isabelle mkdir" for
     1.9 +"isabelle usedir".
    1.10 +
    1.11  * Discontinued support for Poly/ML 5.2.1, which was the last version
    1.12  without exception positions and advanced ML compiler/toplevel
    1.13  configuration.
     2.1 --- a/doc-src/System/Thy/Sessions.thy	Sun Aug 05 16:20:34 2012 +0200
     2.2 +++ b/doc-src/System/Thy/Sessions.thy	Sun Aug 05 20:11:32 2012 +0200
     2.3 @@ -286,4 +286,43 @@
     2.4  \end{ttbox}
     2.5  *}
     2.6  
     2.7 +
     2.8 +section {* Preparing session root directories \label{sec:tool-mkroot} *}
     2.9 +
    2.10 +text {* The @{tool_def mkroot} tool prepares Isabelle session source
    2.11 +  directories, including some @{verbatim ROOT} entry, an example
    2.12 +  theory file, and some initial configuration for document preparation
    2.13 +  (see also \chref{ch:present}).  The usage of @{tool mkroot} is:
    2.14 +
    2.15 +\begin{ttbox}
    2.16 +Usage: isabelle mkroot NAME
    2.17 +
    2.18 +  Prepare session root directory, adding session NAME with
    2.19 +  built-in document preparation.
    2.20 +\end{ttbox}
    2.21 +
    2.22 +  All session-specific files are placed into a separate sub-directory
    2.23 +  given as @{verbatim NAME} above.  The @{verbatim ROOT} file is in
    2.24 +  the parent position relative to that --- it could refer to several
    2.25 +  such sessions.  The @{tool mkroot} tool is conservative in the sense
    2.26 +  that does not overwrite an existing session sub-directory; an
    2.27 +  already existing @{verbatim ROOT} file is extended.
    2.28 +
    2.29 +  The implicit Isabelle settings variable @{setting ISABELLE_LOGIC}
    2.30 +  specifies the parent session, and @{setting
    2.31 +  ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
    2.32 +  into the generated @{verbatim ROOT} file.  *}
    2.33 +
    2.34 +
    2.35 +subsubsection {* Examples *}
    2.36 +
    2.37 +text {* The following produces an example session, relatively to the
    2.38 +  @{verbatim ROOT} in the current directory:
    2.39 +\begin{ttbox}
    2.40 +isabelle mkroot Test && isabelle build -v -d. Test
    2.41 +\end{ttbox}
    2.42 +
    2.43 +  Option @{verbatim "-v"} is not required, but useful to reveal the
    2.44 +  the location of generated documents.  *}
    2.45 +
    2.46  end
     3.1 --- a/doc-src/System/Thy/document/Sessions.tex	Sun Aug 05 16:20:34 2012 +0200
     3.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Sun Aug 05 20:11:32 2012 +0200
     3.3 @@ -402,6 +402,52 @@
     3.4  \end{isamarkuptext}%
     3.5  \isamarkuptrue%
     3.6  %
     3.7 +\isamarkupsection{Preparing session root directories \label{sec:tool-mkroot}%
     3.8 +}
     3.9 +\isamarkuptrue%
    3.10 +%
    3.11 +\begin{isamarkuptext}%
    3.12 +The \indexdef{}{tool}{mkroot}\hypertarget{tool.mkroot}{\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}}} tool prepares Isabelle session source
    3.13 +  directories, including some \verb|ROOT| entry, an example
    3.14 +  theory file, and some initial configuration for document preparation
    3.15 +  (see also \chref{ch:present}).  The usage of \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} is:
    3.16 +
    3.17 +\begin{ttbox}
    3.18 +Usage: isabelle mkroot NAME
    3.19 +
    3.20 +  Prepare session root directory, adding session NAME with
    3.21 +  built-in document preparation.
    3.22 +\end{ttbox}
    3.23 +
    3.24 +  All session-specific files are placed into a separate sub-directory
    3.25 +  given as \verb|NAME| above.  The \verb|ROOT| file is in
    3.26 +  the parent position relative to that --- it could refer to several
    3.27 +  such sessions.  The \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} tool is conservative in the sense
    3.28 +  that does not overwrite an existing session sub-directory; an
    3.29 +  already existing \verb|ROOT| file is extended.
    3.30 +
    3.31 +  The implicit Isabelle settings variable \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}}
    3.32 +  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
    3.33 +  into the generated \verb|ROOT| file.%
    3.34 +\end{isamarkuptext}%
    3.35 +\isamarkuptrue%
    3.36 +%
    3.37 +\isamarkupsubsubsection{Examples%
    3.38 +}
    3.39 +\isamarkuptrue%
    3.40 +%
    3.41 +\begin{isamarkuptext}%
    3.42 +The following produces an example session, relatively to the
    3.43 +  \verb|ROOT| in the current directory:
    3.44 +\begin{ttbox}
    3.45 +isabelle mkroot Test && isabelle build -v -d. Test
    3.46 +\end{ttbox}
    3.47 +
    3.48 +  Option \verb|-v| is not required, but useful to reveal the
    3.49 +  the location of generated documents.%
    3.50 +\end{isamarkuptext}%
    3.51 +\isamarkuptrue%
    3.52 +%
    3.53  \isadelimtheory
    3.54  %
    3.55  \endisadelimtheory
     4.1 --- a/lib/Tools/mkroot	Sun Aug 05 16:20:34 2012 +0200
     4.2 +++ b/lib/Tools/mkroot	Sun Aug 05 20:11:32 2012 +0200
     4.3 @@ -143,7 +143,7 @@
     4.4  fi
     4.5  
     4.6  cat >> "$DIR/ROOT" <<EOF
     4.7 -session "$NAME" = "$ISABELLE_LOGIC" +
     4.8 +session "$NAME"! = "$ISABELLE_LOGIC" +
     4.9    options [document = $ISABELLE_DOC_FORMAT]
    4.10    theories "Ex"
    4.11    files "document/root.tex"
    4.12 @@ -152,19 +152,25 @@
    4.13  
    4.14  # notes
    4.15  
    4.16 +if [ "$DIR" = . ]; then
    4.17 +  OPT_DIR="-d."
    4.18 +else
    4.19 +  OPT_DIR="-d \"$DIR\""
    4.20 +fi
    4.21 +
    4.22  cat <<EOF
    4.23  
    4.24  Notes:
    4.25  
    4.26 -  * $DIR_NAME/Ex.thy contains an example theory
    4.27 +  * $DIR_NAME/Ex.thy contains an example theory.
    4.28  
    4.29 -  * $DIR_NAME/document/root.tex contains the LaTeX master document setup
    4.30 +  * $DIR_NAME/document/root.tex contains the LaTeX master document setup.
    4.31  
    4.32 -  * $DIR/ROOT contains build options, theories and extra file dependencies
    4.33 +  * $DIR/ROOT contains build options, theories and extra file dependencies.
    4.34  
    4.35 -  * the following command line builds the session (with document):
    4.36 +  * The following command line builds the session (with document):
    4.37  
    4.38 -      isabelle build -v -d $DIR ${ISABELLE_LOGIC}-${NAME}
    4.39 +      isabelle build -v $OPT_DIR $NAME
    4.40  
    4.41  EOF
    4.42