--- a/src/Doc/System/Presentation.thy Sun Dec 04 18:49:58 2022 +0100
+++ b/src/Doc/System/Presentation.thy Mon Dec 05 12:17:56 2022 +0100
@@ -65,7 +65,7 @@
\<close>
-section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
+section \<open>Creating session root directories \label{sec:tool-mkroot}\<close>
text \<open>
The @{tool_def mkroot} tool configures a given directory as session root,
@@ -78,8 +78,9 @@
-I init Mercurial repository and add generated files
-T LATEX provide title in LaTeX notation (default: session name)
-n NAME alternative session name (default: directory base name)
+ -q quiet mode: less verbosity
- Prepare session root directory (default: current directory).
+ Create session root directory (default: current directory).
\<close>}
The results are placed in the given directory \<open>dir\<close>, which refers to the
@@ -100,6 +101,8 @@
Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
of the given directory is used.
+ Option \<^verbatim>\<open>-q\<close> reduces verbosity.
+
\<^medskip>
The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
the parent session.
@@ -110,12 +113,12 @@
text \<open>
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>}
+ @{verbatim [display] \<open>isabelle mkroot -q 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 && isabelle build -D .\<close>}
+ @{verbatim [display] \<open>isabelle mkroot -q && isabelle build -D .\<close>}
\<close>
--- a/src/Pure/Tools/mkroot.scala Sun Dec 04 18:49:58 2022 +0100
+++ b/src/Pure/Tools/mkroot.scala Mon Dec 05 12:17:56 2022 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/mkroot.scala
Author: Makarius
-Prepare session root directory.
+Create session root directory.
*/
package isabelle
@@ -24,6 +24,7 @@
init_repos: Boolean = false,
title: String = "",
author: String = "",
+ quiet: Boolean = false,
progress: Progress = new Progress
): Unit = {
Isabelle_System.make_directory(session_dir)
@@ -40,12 +41,12 @@
val root_tex = session_dir + Path.explode("document/root.tex")
- progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
+ progress.echo("\nCreating session " + quote(name) + " in " + session_dir.absolute)
/* ROOT */
- progress.echo(" creating " + root_path)
+ progress.echo_if(!quiet, " creating " + root_path)
File.write(root_path,
"session " + root_name(name) + " = " + root_name(parent) + """ +
@@ -64,7 +65,7 @@
/* document directory */
{
- progress.echo(" creating " + root_tex)
+ progress.echo_if(!quiet, " creating " + root_tex)
Isabelle_System.make_directory(root_tex.dir)
@@ -136,7 +137,7 @@
/* Mercurial repository */
if (init_repos) {
- progress.echo(" \nInitializing Mercurial repository " + session_dir)
+ progress.echo_if(!quiet, " \nInitializing Mercurial repository " + session_dir)
val hg = Mercurial.init_repository(session_dir)
@@ -164,7 +165,7 @@
{
val print_dir = session_dir.implode
- progress.echo("""
+ progress.echo_if(!quiet, """
Now use the following command line to build the session:
isabelle build -D """ +
@@ -176,13 +177,14 @@
/** Isabelle tool wrapper **/
- val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory",
+ val isabelle_tool = Isabelle_Tool("mkroot", "create session root directory",
Scala_Project.here,
{ args =>
var author = ""
var init_repos = false
var title = ""
var session_name = ""
+ var quiet = false
val getopts = Getopts("""
Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
@@ -192,13 +194,15 @@
-I init Mercurial repository and add generated files
-T LATEX provide title in LaTeX notation (default: session name)
-n NAME alternative session name (default: directory base name)
+ -q quiet mode: less verbosity
- Prepare session root directory (default: current directory).
+ Create session root directory (default: current directory).
""",
"A:" -> (arg => author = arg),
- "I" -> (arg => init_repos = true),
+ "I" -> (_ => init_repos = true),
"T:" -> (arg => title = arg),
- "n:" -> (arg => session_name = arg))
+ "n:" -> (arg => session_name = arg),
+ "q" -> (_ => quiet = true))
val more_args = getopts(args)
@@ -209,7 +213,9 @@
case _ => getopts.usage()
}
+ val progress = new Console_Progress
+
mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
- author = author, title = title, progress = new Console_Progress)
+ author = author, title = title, quiet = quiet, progress = progress)
})
}