adapted to changed ROOT syntax (see 13857f49d215);
authorwenzelm
Sat Nov 11 14:55:30 2017 +0100 (19 months ago)
changeset 67042677cab7c2b85
parent 67041 f8b0367046bd
child 67043 848672fcaee5
adapted to changed ROOT syntax (see 13857f49d215);
discontinued pointless option -d: always enabled;
src/Doc/System/Presentation.thy
src/Doc/Tutorial/Documents/Documents.thy
src/Pure/Tools/mkroot.scala
     1.1 --- a/src/Doc/System/Presentation.thy	Sat Nov 11 14:35:41 2017 +0100
     1.2 +++ b/src/Doc/System/Presentation.thy	Sat Nov 11 14:55:30 2017 +0100
     1.3 @@ -97,7 +97,6 @@
     1.4  \<open>Usage: isabelle mkroot [OPTIONS] [DIR]
     1.5  
     1.6    Options are:
     1.7 -    -d           enable document preparation
     1.8      -n NAME      alternative session name (default: DIR base name)
     1.9  
    1.10    Prepare session root DIR (default: current directory).\<close>}
    1.11 @@ -107,10 +106,9 @@
    1.12    sense that it does not overwrite existing files or directories. Earlier
    1.13    attempts to generate a session root need to be deleted manually.
    1.14  
    1.15 -  \<^medskip>
    1.16 -  Option \<^verbatim>\<open>-d\<close> indicates that the session shall be accompanied by a formal
    1.17 -  document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see
    1.18 -  also \chref{ch:present}).
    1.19 +  The generated session template will be accompanied by a formal document,
    1.20 +  with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also
    1.21 +  \chref{ch:present}).
    1.22  
    1.23    Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
    1.24    base name of the given directory is used.
    1.25 @@ -125,14 +123,13 @@
    1.26  subsubsection \<open>Examples\<close>
    1.27  
    1.28  text \<open>
    1.29 -  Produce session \<^verbatim>\<open>Test\<close> (with document preparation) within a separate
    1.30 -  directory of the same name:
    1.31 -  @{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
    1.32 +  Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name:
    1.33 +  @{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>}
    1.34  
    1.35    \<^medskip>
    1.36    Upgrade the current directory into a session ROOT with document preparation,
    1.37    and build it:
    1.38 -  @{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
    1.39 +  @{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>}
    1.40  \<close>
    1.41  
    1.42  
     2.1 --- a/src/Doc/Tutorial/Documents/Documents.thy	Sat Nov 11 14:35:41 2017 +0100
     2.2 +++ b/src/Doc/Tutorial/Documents/Documents.thy	Sat Nov 11 14:55:30 2017 +0100
     2.3 @@ -351,7 +351,7 @@
     2.4    preparation) may be produced as follows:
     2.5  
     2.6  \begin{verbatim}
     2.7 -  isabelle mkroot -d MySession
     2.8 +  isabelle mkroot MySession
     2.9    isabelle build -D MySession
    2.10  \end{verbatim}
    2.11  
     3.1 --- a/src/Pure/Tools/mkroot.scala	Sat Nov 11 14:35:41 2017 +0100
     3.2 +++ b/src/Pure/Tools/mkroot.scala	Sat Nov 11 14:55:30 2017 +0100
     3.3 @@ -22,7 +22,6 @@
     3.4      session_name: String = "",
     3.5      session_dir: Path = Path.current,
     3.6      session_parent: String = "",
     3.7 -    document: Boolean = false,
     3.8      title: String = "",
     3.9      author: String = "",
    3.10      progress: Progress = No_Progress)
    3.11 @@ -36,7 +35,7 @@
    3.12      if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
    3.13  
    3.14      val document_path = session_dir + Path.explode("document")
    3.15 -    if (document && document_path.file.exists) error("Cannot overwrite existing " + document_path)
    3.16 +    if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
    3.17  
    3.18      progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
    3.19  
    3.20 @@ -46,29 +45,22 @@
    3.21      progress.echo("  creating " + root_path)
    3.22  
    3.23      File.write(root_path,
    3.24 -      "session " + root_name(name) + " = " + root_name(parent) + " +" +
    3.25 -      (if (document) """
    3.26 +      "session " + root_name(name) + " = " + root_name(parent) + """ +
    3.27    options [document = pdf, document_output = "output"]
    3.28 -  theories [document = false]
    3.29 -    (* Foo *)
    3.30 -    (* Bar *)
    3.31 +(*theories [document = false]
    3.32 +    A
    3.33 +    B
    3.34    theories
    3.35 -    (* Baz *)
    3.36 +    C
    3.37 +    D*)
    3.38    document_files
    3.39      "root.tex"
    3.40 -"""
    3.41 -      else """
    3.42 -  options [document = false]
    3.43 -  theories
    3.44 -    (* Foo *)
    3.45 -    (* Bar *)
    3.46 -    (* Baz *)
    3.47 -"""))
    3.48 +""")
    3.49  
    3.50  
    3.51      /* document directory */
    3.52  
    3.53 -    if (document) {
    3.54 +    {
    3.55        val root_tex = session_dir + Path.explode("document/root.tex")
    3.56        progress.echo("  creating " + root_tex)
    3.57  
    3.58 @@ -157,19 +149,16 @@
    3.59  
    3.60    val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
    3.61    {
    3.62 -    var document = false
    3.63      var session_name = ""
    3.64  
    3.65      val getopts = Getopts("""
    3.66  Usage: isabelle mkroot [OPTIONS] [DIR]
    3.67  
    3.68    Options are:
    3.69 -    -d           enable document preparation
    3.70      -n NAME      alternative session name (default: DIR base name)
    3.71  
    3.72    Prepare session root DIR (default: current directory).
    3.73  """,
    3.74 -      "d" -> (_ => document = true),
    3.75        "n:" -> (arg => session_name = arg))
    3.76  
    3.77      val more_args = getopts(args)
    3.78 @@ -181,7 +170,6 @@
    3.79          case _ => getopts.usage()
    3.80        }
    3.81  
    3.82 -    mkroot(session_name = session_name, session_dir = session_dir, document = document,
    3.83 -      progress = new Console_Progress)
    3.84 +    mkroot(session_name = session_name, session_dir = session_dir, progress = new Console_Progress)
    3.85    })
    3.86  }