--- a/NEWS Sat Nov 11 14:55:30 2017 +0100
+++ b/NEWS Sat Nov 11 15:45:12 2017 +0100
@@ -98,6 +98,9 @@
for this session. There is no need to specify options [document = false]
anymore.
+* The command-line tool "isabelle mkroot" now always produces a document
+outline: its options have been adapted accordingly. INCOMPATIBILITY.
+
* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
support has been discontinued.
--- a/src/Doc/System/Presentation.thy Sat Nov 11 14:55:30 2017 +0100
+++ b/src/Doc/System/Presentation.thy Sat Nov 11 15:45:12 2017 +0100
@@ -94,12 +94,15 @@
The @{tool_def mkroot} tool configures a given directory as session root,
with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is:
@{verbatim [display]
-\<open>Usage: isabelle mkroot [OPTIONS] [DIR]
+\<open>Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
Options are:
- -n NAME alternative session name (default: DIR base name)
+ -A LATEX provide author in LaTeX notation (default: user name)
+ -T LATEX provide title in LaTeX notation (default: session name)
+ -n NAME alternative session name (default: directory base name)
- Prepare session root DIR (default: current directory).\<close>}
+ Prepare session root directory (default: current directory).
+\<close>}
The results are placed in the given directory \<open>dir\<close>, which refers to the
current directory by default. The @{tool mkroot} tool is conservative in the
@@ -107,16 +110,18 @@
attempts to generate a session root need to be deleted manually.
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
+ with \<open>DIRECTORY\<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.
+ Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
+ using {\LaTeX} source notation.
+
+ Option \<^verbatim>\<open>-n\<close> specifies 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>\<open>ROOT\<close> file.
+ the parent session.
\<close>
--- a/src/Pure/Tools/mkroot.scala Sat Nov 11 14:55:30 2017 +0100
+++ b/src/Pure/Tools/mkroot.scala Sat Nov 11 15:45:12 2017 +0100
@@ -105,8 +105,7 @@
\begin{document}
\title{""" + (proper_string(title) getOrElse latex_name(name)) + """}
-\author{""" +
- (proper_string(author) getOrElse ("By " + latex_name(Isabelle_System.getenv("USER")))) + """}
+\author{""" + (proper_string(author) getOrElse latex_name(System.getProperty("user.name"))) + """}
\maketitle
\tableofcontents
@@ -149,16 +148,22 @@
val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
{
+ var author = ""
+ var title = ""
var session_name = ""
val getopts = Getopts("""
-Usage: isabelle mkroot [OPTIONS] [DIR]
+Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
Options are:
- -n NAME alternative session name (default: DIR base name)
+ -A LATEX provide author in LaTeX notation (default: user name)
+ -T LATEX provide title in LaTeX notation (default: session name)
+ -n NAME alternative session name (default: directory base name)
- Prepare session root DIR (default: current directory).
+ Prepare session root directory (default: current directory).
""",
+ "A:" -> (arg => author = arg),
+ "T:" -> (arg => title = arg),
"n:" -> (arg => session_name = arg))
val more_args = getopts(args)
@@ -170,6 +175,7 @@
case _ => getopts.usage()
}
- mkroot(session_name = session_name, session_dir = session_dir, progress = new Console_Progress)
+ mkroot(session_name = session_name, session_dir = session_dir, author = author, title = title,
+ progress = new Console_Progress)
})
}