# HG changeset patch
# User wenzelm
# Date 1510411512 -3600
# Node ID 848672fcaee58bdd6c38ce45f0284084d3c7fd14
# Parent  677cab7c2b85c3eed329fc58324289bc1b993bda
more options for "isabelle mkroot";
updated documentation;

diff -r 677cab7c2b85 -r 848672fcaee5 NEWS
--- 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.
 
diff -r 677cab7c2b85 -r 848672fcaee5 src/Doc/System/Presentation.thy
--- 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>
 
 
diff -r 677cab7c2b85 -r 848672fcaee5 src/Pure/Tools/mkroot.scala
--- 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)
   })
 }