refined isabelle mkroot;
allow empty 'theories' to facilitate generated templates;

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

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

--- 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" <<EOF
-header {* Some example theory *}
+echo "  creating $DIR/ROOT"
 
-theory Ex imports Main
-begin
-
-text {* Some text here. *}
-
-end
+if [ "$DOC" = true ]; then
+  cat > "$DIR/ROOT" <<EOF
+session "$NAME" = "$ISABELLE_LOGIC" +
+  options [document = $ISABELLE_DOC_FORMAT]
+  theories [document = false]
+    (* Foo Bar *)
+  theories
+    (* Baz *)
+  files "document/root.tex"
 EOF
+else
+  cat > "$DIR/ROOT" <<EOF
+session "$NAME" = "$ISABELLE_LOGIC" +
+  options [document = false]
+  theories
+    (* Foo Bar Baz *)
+EOF
+fi
 
 
 # document directory
 
-echo "creating $DIR_NAME/document/root.tex"
-
-mkdir "$DIR_NAME/document" || fail "Bad directory: \"$DIR_NAME/document\""
+if [ "$DOC" = true ]; then
+  echo "  creating $DIR/document/root.tex"
 
-TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
-AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
-cat > "$DIR_NAME/document/root.tex" <<EOF
+  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
+  
+  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
+  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
+
+  cat > "$DIR/document/root.tex" <<EOF
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 
@@ -131,46 +177,22 @@
 %%% TeX-master: t
 %%% End:
 EOF
-
-
-# ROOT
-
-if [ -e "$DIR/ROOT" ]; then
-  echo "appending to existing ROOT"
-  echo >> "$DIR/ROOT"
-else
-  echo "creating ROOT"
 fi
 
-cat >> "$DIR/ROOT" <<EOF
-session "$NAME"! = "$ISABELLE_LOGIC" +
-  options [document = $ISABELLE_DOC_FORMAT]
-  theories "Ex"
-  files "document/root.tex"
-EOF
-
-
 # notes
 
-if [ "$DIR" = . ]; then
-  OPT_DIR="-d."
+declare -a DIR_PARTS=($DIR)
+if [ ${#DIR_PARTS[@]} = 1 ]; then
+  OPT_DIR="-D $DIR"
 else
-  OPT_DIR="-d \"$DIR\""
+  OPT_DIR="-D \"$DIR\""
 fi
 
 cat <<EOF
 
-Notes:
-
-  * $DIR_NAME/Ex.thy contains an example theory.
-
-  * $DIR_NAME/document/root.tex contains the LaTeX master document setup.
+Now use the following command line to build the session:
 
-  * $DIR/ROOT contains build options, theories and extra file dependencies.
-
-  * The following command line builds the session (with document):
-
-      isabelle build -v $OPT_DIR $NAME
+  isabelle build -v $OPT_DIR
 
 EOF
 

--- a/src/Pure/System/build.scala	Wed Aug 08 17:49:56 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Aug 08 20:35:34 2012 +0200
@@ -172,7 +172,7 @@
       val options = keyword("[") ~> 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 }) ~