adapted to changed ROOT syntax (see 13857f49d215);
discontinued pointless option -d: always enabled;
--- 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>
--- 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}
--- 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)
})
}