src/Pure/Admin/build_doc.scala
changeset 75394 42267c650205
parent 75393 87ebf5a50283
child 75758 5ad049a5f6a8
--- a/src/Pure/Admin/build_doc.scala	Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_doc.scala	Fri Apr 01 23:19:12 2022 +0200
@@ -73,14 +73,15 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args => {
-      var all_docs = false
-      var max_jobs = 1
-      var sequential = false
-      var options = Options.init()
+    Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here,
+      { args =>
+        var all_docs = false
+        var max_jobs = 1
+        var sequential = false
+        var options = Options.init()
 
-      val getopts =
-        Getopts("""
+        val getopts =
+          Getopts("""
 Usage: isabelle build_doc [OPTIONS] [DOCS ...]
 
   Options are:
@@ -92,20 +93,20 @@
   Build Isabelle documentation from documentation sessions with
   suitable document_variants entry.
 """,
-          "a" -> (_ => all_docs = true),
-          "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
-          "o:" -> (arg => options = options + arg),
-          "s" -> (_ => sequential = true))
+            "a" -> (_ => all_docs = true),
+            "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+            "o:" -> (arg => options = options + arg),
+            "s" -> (_ => sequential = true))
 
-      val docs = getopts(args)
+        val docs = getopts(args)
 
-      if (!all_docs && docs.isEmpty) getopts.usage()
+        if (!all_docs && docs.isEmpty) getopts.usage()
 
-      val progress = new Console_Progress()
+        val progress = new Console_Progress()
 
-      progress.interrupt_handler {
-        build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs,
-          sequential = sequential, docs = docs)
-      }
-    })
+        progress.interrupt_handler {
+          build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs,
+            sequential = sequential, docs = docs)
+        }
+      })
 }