# HG changeset patch # User wenzelm # Date 1344450934 -7200 # Node ID 3a6c03b15916fb90e922c4730b9a328cd8533e40 # Parent f8c1a5b9488f5f968cc89afebdf71cb7b1cf4926 refined isabelle mkroot; allow empty 'theories' to facilitate generated templates; diff -r f8c1a5b9488f -r 3a6c03b15916 doc-src/System/Thy/Sessions.thy --- a/doc-src/System/Thy/Sessions.thy Wed Aug 08 17:49:56 2012 +0200 +++ b/doc-src/System/Thy/Sessions.thy Wed Aug 08 20:35:34 2012 +0200 @@ -64,7 +64,7 @@ ; value: @{syntax name} | @{syntax real} ; - theories: @'theories' opts? ( @{syntax name} + ) + theories: @'theories' opts? ( @{syntax name} * ) ; files: @'files' ( @{syntax name} + ) "} @@ -321,40 +321,55 @@ 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: +text {* The @{tool_def mkroot} tool configures a given directory as + session root, with some @{verbatim ROOT} file and optional document + source directory. Its usage is: +\begin{ttbox} +Usage: isabelle mkroot [OPTIONS] [DIR] -\begin{ttbox} -Usage: isabelle mkroot NAME + Options are: + -d enable document preparation + -n NAME alternative session name (default: DIR base name) - Prepare session root directory, adding session NAME with - built-in document preparation. + Prepare session root DIR (default: current directory). \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 results are placed in the given directory @{text dir}, which + refers to the current directory by default. The @{tool mkroot} tool + is conservative in the sense that it does not overwrite existing + files or directories. Earlier attempts to generate a session root + need to be deleted manually. - The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} - specifies the parent session, and @{setting + \medskip Option @{verbatim "-d"} indicates that the session shall be + accompanied by a formal document, with @{text dir}@{verbatim + "/document/root.tex"} as its {\LaTeX} entry point (see also + \chref{ch:present}). + + Option @{verbatim "-n"} allows to specify an alternative session + name; otherwise the base name of the given directory is used. + + \medskip 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: +text {* The following produces an example session as separate + directory called @{verbatim Test}: \begin{ttbox} -isabelle mkroot Test && isabelle build -v -d. Test +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. *} + the location of generated documents. + + \medskip The subsequent example turns the current directory to a + session directory with document and builds it: +\begin{ttbox} +isabelle mkroot -d && isabelle build -D. +\end{ttbox} +*} end diff -r f8c1a5b9488f -r 3a6c03b15916 doc-src/System/Thy/document/Sessions.tex --- a/doc-src/System/Thy/document/Sessions.tex Wed Aug 08 17:49:56 2012 +0200 +++ b/doc-src/System/Thy/document/Sessions.tex Wed Aug 08 20:35:34 2012 +0200 @@ -158,8 +158,8 @@ \rail@nont{\isa{opts}}[] \rail@endbar \rail@plus -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@nextplus{1} +\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@endplus \rail@end \rail@begin{2}{\isa{files}} @@ -435,27 +435,33 @@ \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: +The \indexdef{}{tool}{mkroot}\hypertarget{tool.mkroot}{\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}}} tool configures a given directory as + session root, with some \verb|ROOT| file and optional document + source directory. Its usage is: +\begin{ttbox} +Usage: isabelle mkroot [OPTIONS] [DIR] -\begin{ttbox} -Usage: isabelle mkroot NAME + Options are: + -d enable document preparation + -n NAME alternative session name (default: DIR base name) - Prepare session root directory, adding session NAME with - built-in document preparation. + Prepare session root DIR (default: current directory). \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 results are placed in the given directory \isa{dir}, which + refers to the current directory by default. The \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} tool + is conservative in the sense that it does not overwrite existing + files or directories. Earlier attempts to generate a session root + need to be deleted manually. - 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 + \medskip Option \verb|-d| indicates that the session shall be + accompanied by a formal document, with \isa{dir}\verb|/document/root.tex| as its {\LaTeX} entry point (see also + \chref{ch:present}). + + Option \verb|-n| allows to specify an alternative session + name; otherwise the base name of the given directory is used. + + \medskip 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% @@ -465,14 +471,20 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The following produces an example session, relatively to the - \verb|ROOT| in the current directory: +The following produces an example session as separate + directory called \verb|Test|: \begin{ttbox} -isabelle mkroot Test && isabelle build -v -d. Test +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.% + the location of generated documents. + + \medskip The subsequent example turns the current directory to a + session directory with document and builds it: +\begin{ttbox} +isabelle mkroot -d && isabelle build -D. +\end{ttbox}% \end{isamarkuptext}% \isamarkuptrue% % diff -r f8c1a5b9488f -r 3a6c03b15916 lib/Tools/mkroot --- a/lib/Tools/mkroot Wed Aug 08 17:49:56 2012 +0200 +++ b/lib/Tools/mkroot Wed Aug 08 20:35:34 2012 +0200 @@ -12,10 +12,13 @@ function usage() { echo - echo "Usage: isabelle $PRG NAME" + echo "Usage: isabelle $PRG [OPTIONS] [DIR]" echo - echo " Prepare session root directory, adding session NAME with" - echo " built-in document preparation." + echo " Options are:" + echo " -d enable document preparation" + echo " -n NAME alternative session name (default: DIR base name)" + echo + echo " Prepare session root DIR (default: current directory)." echo exit 1 } @@ -29,48 +32,91 @@ ## process command line -[ "$#" -ne 1 -o "$1" = "-?" ] && usage +# options + +DOC="" +NAME="" -DIR_NAME="$1"; shift +while getopts "n:d" OPT +do + case "$OPT" in + d) + DOC="true" + ;; + n) + NAME="$OPTARG" + ;; + \?) + usage + ;; + esac +done -DIR="$(dirname "$DIR_NAME")" -NAME="$(basename "$DIR_NAME")" +shift $(($OPTIND - 1)) + + +# args + +if [ "$#" -eq 0 ]; then + DIR="." +elif [ "$#" -eq 1 ]; then + DIR="$1" + shift +else + usage +fi ## main -[ -e "$DIR_NAME" ] && fail "Cannot overwrite existing \"$DIR_NAME\"" +mkdir -p "$DIR" || fail "Bad directory: \"$DIR\"" + +[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")" + +[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT" + +[ "$DOC" = true -a -e "$DIR/document" ] && \ + fail "Cannot overwrite existing $DIR/document" echo -echo "Preparing session \"$NAME\" ..." - -mkdir -p "$DIR_NAME" || fail "Bad directory: \"$DIR_NAME\"" +echo "Preparing session \"$NAME\" in \"$DIR\"" -# example theory +# ROOT -echo "creating $DIR_NAME/Ex.thy" -cat > "$DIR_NAME/Ex.thy" < "$DIR/ROOT" < "$DIR/ROOT" < "$DIR_NAME/document/root.tex" < "$DIR/document/root.tex" <> "$DIR/ROOT" -else - echo "creating ROOT" fi -cat >> "$DIR/ROOT" < repsep(option, keyword(",")) <~ keyword("]") val theories = - keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^ + keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^ { case _ ~ (x ~ y) => (x, y) } ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~