# HG changeset patch
# User wenzelm
# Date 1670239076 -3600
# Node ID c7f3e94fce7b48f0d7782d09e50ec44e046dfc7d
# Parent  e28aed61a4b1fc836672f1a8832c73e2ac1f4ad6
tuned messages and options;

diff -r e28aed61a4b1 -r c7f3e94fce7b src/Doc/System/Presentation.thy
--- 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>
 
 
diff -r e28aed61a4b1 -r c7f3e94fce7b src/Pure/Tools/mkroot.scala
--- 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)
     })
 }