src/Doc/System/Presentation.thy
changeset 67043 848672fcaee5
parent 67042 677cab7c2b85
child 67069 f11486d31586
     1.1 --- a/src/Doc/System/Presentation.thy	Sat Nov 11 14:55:30 2017 +0100
     1.2 +++ b/src/Doc/System/Presentation.thy	Sat Nov 11 15:45:12 2017 +0100
     1.3 @@ -94,12 +94,15 @@
     1.4    The @{tool_def mkroot} tool configures a given directory as session root,
     1.5    with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is:
     1.6    @{verbatim [display]
     1.7 -\<open>Usage: isabelle mkroot [OPTIONS] [DIR]
     1.8 +\<open>Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
     1.9  
    1.10    Options are:
    1.11 -    -n NAME      alternative session name (default: DIR base name)
    1.12 +    -A LATEX     provide author in LaTeX notation (default: user name)
    1.13 +    -T LATEX     provide title in LaTeX notation (default: session name)
    1.14 +    -n NAME      alternative session name (default: directory base name)
    1.15  
    1.16 -  Prepare session root DIR (default: current directory).\<close>}
    1.17 +  Prepare session root directory (default: current directory).
    1.18 +\<close>}
    1.19  
    1.20    The results are placed in the given directory \<open>dir\<close>, which refers to the
    1.21    current directory by default. The @{tool mkroot} tool is conservative in the
    1.22 @@ -107,16 +110,18 @@
    1.23    attempts to generate a session root need to be deleted manually.
    1.24  
    1.25    The generated session template will be accompanied by a formal document,
    1.26 -  with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also
    1.27 +  with \<open>DIRECTORY\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also
    1.28    \chref{ch:present}).
    1.29  
    1.30 -  Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
    1.31 -  base name of the given directory is used.
    1.32 +  Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
    1.33 +  using {\LaTeX} source notation.
    1.34 +
    1.35 +  Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
    1.36 +  of the given directory is used.
    1.37  
    1.38    \<^medskip>
    1.39    The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
    1.40 -  the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document
    1.41 -  format to be filled filled into the generated \<^verbatim>\<open>ROOT\<close> file.
    1.42 +  the parent session.
    1.43  \<close>
    1.44  
    1.45