# HG changeset patch
# User wenzelm
# Date 1510408530 -3600
# Node ID 677cab7c2b85c3eed329fc58324289bc1b993bda
# Parent  f8b0367046bd1383212014346f3865af8cc4d56c
adapted to changed ROOT syntax (see 13857f49d215);
discontinued pointless option -d: always enabled;

diff -r f8b0367046bd -r 677cab7c2b85 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Sat Nov 11 14:35:41 2017 +0100
+++ b/src/Doc/System/Presentation.thy	Sat Nov 11 14:55:30 2017 +0100
@@ -97,7 +97,6 @@
 \<open>Usage: isabelle mkroot [OPTIONS] [DIR]
 
   Options are:
-    -d           enable document preparation
     -n NAME      alternative session name (default: DIR base name)
 
   Prepare session root DIR (default: current directory).\<close>}
@@ -107,10 +106,9 @@
   sense that it does not overwrite existing files or directories. Earlier
   attempts to generate a session root need to be deleted manually.
 
-  \<^medskip>
-  Option \<^verbatim>\<open>-d\<close> indicates that the session shall be accompanied by a formal
-  document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see
-  also \chref{ch:present}).
+  The generated session template will be accompanied by a formal document,
+  with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also
+  \chref{ch:present}).
 
   Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
   base name of the given directory is used.
@@ -125,14 +123,13 @@
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Produce session \<^verbatim>\<open>Test\<close> (with document preparation) within a separate
-  directory of the same name:
-  @{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
+  Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name:
+  @{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>}
 
   \<^medskip>
   Upgrade the current directory into a session ROOT with document preparation,
   and build it:
-  @{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
+  @{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>}
 \<close>
 
 
diff -r f8b0367046bd -r 677cab7c2b85 src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Sat Nov 11 14:35:41 2017 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Sat Nov 11 14:55:30 2017 +0100
@@ -351,7 +351,7 @@
   preparation) may be produced as follows:
 
 \begin{verbatim}
-  isabelle mkroot -d MySession
+  isabelle mkroot MySession
   isabelle build -D MySession
 \end{verbatim}
 
diff -r f8b0367046bd -r 677cab7c2b85 src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Sat Nov 11 14:35:41 2017 +0100
+++ b/src/Pure/Tools/mkroot.scala	Sat Nov 11 14:55:30 2017 +0100
@@ -22,7 +22,6 @@
     session_name: String = "",
     session_dir: Path = Path.current,
     session_parent: String = "",
-    document: Boolean = false,
     title: String = "",
     author: String = "",
     progress: Progress = No_Progress)
@@ -36,7 +35,7 @@
     if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
 
     val document_path = session_dir + Path.explode("document")
-    if (document && document_path.file.exists) error("Cannot overwrite existing " + document_path)
+    if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
 
     progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
 
@@ -46,29 +45,22 @@
     progress.echo("  creating " + root_path)
 
     File.write(root_path,
-      "session " + root_name(name) + " = " + root_name(parent) + " +" +
-      (if (document) """
+      "session " + root_name(name) + " = " + root_name(parent) + """ +
   options [document = pdf, document_output = "output"]
-  theories [document = false]
-    (* Foo *)
-    (* Bar *)
+(*theories [document = false]
+    A
+    B
   theories
-    (* Baz *)
+    C
+    D*)
   document_files
     "root.tex"
-"""
-      else """
-  options [document = false]
-  theories
-    (* Foo *)
-    (* Bar *)
-    (* Baz *)
-"""))
+""")
 
 
     /* document directory */
 
-    if (document) {
+    {
       val root_tex = session_dir + Path.explode("document/root.tex")
       progress.echo("  creating " + root_tex)
 
@@ -157,19 +149,16 @@
 
   val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
   {
-    var document = false
     var session_name = ""
 
     val getopts = Getopts("""
 Usage: isabelle mkroot [OPTIONS] [DIR]
 
   Options are:
-    -d           enable document preparation
     -n NAME      alternative session name (default: DIR base name)
 
   Prepare session root DIR (default: current directory).
 """,
-      "d" -> (_ => document = true),
       "n:" -> (arg => session_name = arg))
 
     val more_args = getopts(args)
@@ -181,7 +170,6 @@
         case _ => getopts.usage()
       }
 
-    mkroot(session_name = session_name, session_dir = session_dir, document = document,
-      progress = new Console_Progress)
+    mkroot(session_name = session_name, session_dir = session_dir, progress = new Console_Progress)
   })
 }