From d93e1383d44716ff45afb804b916e2c4c33e455d Mon Sep 17 00:00:00 2001
From: Makarius <makarius@sketis.net>
Date: Sat, 3 Dec 2022 12:29:24 +0100
Subject: [PATCH] Afford full-scale command-line tool

---
 .woodpecker/mk_release    |  5 ++--
 src/scala/dof.scala       | 58 +++++++++++++++++++++++++++++++++------
 src/scala/dof_tools.scala |  3 +-
 3 files changed, 54 insertions(+), 12 deletions(-)

diff --git a/.woodpecker/mk_release b/.woodpecker/mk_release
index 47a1ecf..beeeb61 100755
--- a/.woodpecker/mk_release
+++ b/.woodpecker/mk_release
@@ -194,9 +194,8 @@ for i in $VARS; do
         export "$i"
 done
 
-$ISABELLE_TOOL scala_build
-ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL java isabelle.dof.DOF isabelle_version)"
-DOF_VERSION="$($ISABELLE_TOOL java isabelle.dof.DOF dof_version)"
+ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL dof_param -b isabelle_version)"
+DOF_VERSION="$($ISABELLE_TOOL dof_param -b dof_version)"
 
 ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
 ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
diff --git a/src/scala/dof.scala b/src/scala/dof.scala
index d8c1dac..b42759b 100644
--- a/src/scala/dof.scala
+++ b/src/scala/dof.scala
@@ -66,13 +66,55 @@ object DOF {
 
   def options(opts: Options): Options = opts + "document_comment_latex"
 
-  def main(args: Array[String]): Unit = {
-    args.toList match {
-      case List("isabelle_version") => println(isabelle_version)
-      case List("dof_version") => println(version)
-      case bad =>
-        error("Bad Java command-line arguments" +
-          (if (bad.isEmpty) "" else bad.mkString(":\n  ", "\n  ", "")))
-    }
+
+
+  /** Isabelle tool wrapper **/
+
+  sealed case class Parameter(name: String, value: String) {
+    override def toString: String = name
+
+    def print(value_only: Boolean): String =
+      if (value_only) value else name + "=" + value
   }
+
+  val parameters: List[Parameter] =
+    List(
+      Parameter("isabelle_version", isabelle_version),
+      Parameter("dof_version", version))
+
+  def print_parameters(names: List[String],
+    all: Boolean = false,
+    value_only: Boolean = false,
+    progress: Progress = new Progress
+  ): Unit = {
+    val bad = names.filter(name => !parameters.exists(_.name == name))
+    if (bad.nonEmpty) error("Unknown parameter(s): " + commas_quote(bad))
+
+    val params = if (all) parameters else parameters.filter(p => names.contains(p.name))
+    for (p <- params) progress.echo(p.print(value_only))
+  }
+
+  val isabelle_tool = Isabelle_Tool("dof_param", "print Isabelle/DOF parameters",
+    Scala_Project.here, args =>
+  {
+    var all = false
+    var value_only = false
+
+    val getopts = Getopts("""
+Usage: isabelle dof_param [OPTIONS] NAMES
+
+  Options are:
+    -a           print all parameters
+    -b           print values only (default: NAME=VALUE)
+
+  Print given Isabelle/DOF parameters, with names from the list:
+  """ + commas_quote(parameters.map(_.toString)),
+      "a" -> (_ => all = true),
+      "b" -> (_ => value_only = true))
+
+    val names = getopts(args)
+    if (names.isEmpty && !all) getopts.usage()
+
+    print_parameters(names, all = all, value_only = value_only, progress = new Console_Progress)
+  })
 }
diff --git a/src/scala/dof_tools.scala b/src/scala/dof_tools.scala
index e859f05..646eb41 100644
--- a/src/scala/dof_tools.scala
+++ b/src/scala/dof_tools.scala
@@ -37,5 +37,6 @@ import isabelle._
 
 
 class DOF_Tools extends Isabelle_Scala_Tools(
-  DOF_Mkroot.isabelle_tool
+  DOF.isabelle_tool,
+  DOF_Mkroot.isabelle_tool,
 )