forked from Isabelle_DOF/Isabelle_DOF
Afford full-scale command-line tool
This commit is contained in:
parent
3d5d1e7476
commit
d93e1383d4
|
@ -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
|
||||
|
|
|
@ -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)
|
||||
})
|
||||
}
|
||||
|
|
|
@ -37,5 +37,6 @@ import isabelle._
|
|||
|
||||
|
||||
class DOF_Tools extends Isabelle_Scala_Tools(
|
||||
DOF_Mkroot.isabelle_tool
|
||||
DOF.isabelle_tool,
|
||||
DOF_Mkroot.isabelle_tool,
|
||||
)
|
||||
|
|
Reference in New Issue