--- a/NEWS Fri Nov 24 22:22:41 2023 +0100
+++ b/NEWS Sat Nov 25 16:13:08 2023 +0100
@@ -73,6 +73,10 @@
*** System ***
+* Directory src/Tools/Demo provides an Isabelle system component with
+command-line tool that is implemented in Isabelle/Scala. It serves as
+demonstration for user-defined tools.
+
* The Isabelle/Scala module isabelle.Registry provides hierarchic system
configuration, based on a collection of TOML files (see also
https://toml.io/en/v1.0.0). The settings variable ISABELLE_REGISTRY
--- a/etc/components Fri Nov 24 22:22:41 2023 +0100
+++ b/etc/components Sat Nov 25 16:13:08 2023 +0100
@@ -1,4 +1,5 @@
#built-in components
+src/Tools/Demo
src/Tools/jEdit
src/Tools/GraphBrowser
src/Tools/Graphview
--- a/src/Doc/System/Scala.thy Fri Nov 24 22:22:41 2023 +0100
+++ b/src/Doc/System/Scala.thy Sat Nov 25 16:13:08 2023 +0100
@@ -46,7 +46,8 @@
\<^medskip>
There is also an implicit build process for Isabelle/Scala/Java modules,
based on \<^path>\<open>etc/build.props\<close> within the component directory (see also
- \secref{sec:scala-build}).
+ \secref{sec:scala-build}). See \<^file>\<open>$ISABELLE_HOME/src/Tools/Demo/README.md\<close>
+ for an example components with command-line tools in Isabelle/Scala.
\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Demo/README.md Sat Nov 25 16:13:08 2023 +0100
@@ -0,0 +1,10 @@
+# Demo: Isabelle system component and Isabelle/Scala tool
+
+This directory constitutes an Isabelle system component. It defines an
+Isabelle/Scala tool that is available via the command-line as "isabelle demo".
+
+See also "isabelle doc system" on "isabelle components -u" to register system
+components in user-space.
+
+NOTE: User-defined components should chose a name prefix that is unlikely to
+clash with existing tools (or other user tools).
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Demo/etc/build.props Sat Nov 25 16:13:08 2023 +0100
@@ -0,0 +1,8 @@
+title = Demo
+module = lib/demo.jar
+requirements = \
+ env:ISABELLE_SCALA_JAR
+sources = \
+ src/demo_tool.scala
+services = \
+ isabelle.demo.Tools
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Demo/etc/options Sat Nov 25 16:13:08 2023 +0100
@@ -0,0 +1,6 @@
+(* :mode=isabelle-options: *)
+
+section "Demo"
+
+option demo_prefix : string = ""
+ -- "line prefix for output of arguments"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Demo/etc/settings Sat Nov 25 16:13:08 2023 +0100
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_DEMO_HOME="$COMPONENT"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Demo/src/demo_tool.scala Sat Nov 25 16:13:08 2023 +0100
@@ -0,0 +1,59 @@
+/* Title: Tools/Demo/src/demo_tool.scala
+ Author: Makarius
+
+Isabelle command-line tool demo.
+*/
+
+package isabelle.demo
+
+import isabelle._
+
+
+object Demo_Tool {
+ /* component resources */
+
+ def home: Path = Path.explode("$ISABELLE_DEMO_HOME")
+ def readme: Path = home + Path.explode("README.md")
+
+
+ /* main entry point in Scala */
+
+ def demo(options: Options, args: List[String], progress: Progress = new Progress): Unit = {
+ val prefix = options.string("demo_prefix")
+ for (arg <- args) progress.echo(Library.prefix_lines(prefix, arg))
+ if (progress.verbose) progress.echo("\nSee also " + readme.expand)
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("demo", "Isabelle command-line tool demo",
+ Scala_Project.here, { args =>
+ var options = Options.init()
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle demo [OPTIONS] ARGS ...
+
+ Options are:
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose mode: print more explanations
+
+ Echo given arguments, with optional verbose mode. Example:
+
+ isabelle demo -v -o demo_prefix="+++ " A B C
+""",
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true))
+
+ val more_args = getopts(args)
+ if (more_args.isEmpty) getopts.usage()
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ demo(options, more_args, progress = progress)
+ })
+}
+
+class Tools extends Isabelle_Scala_Tools(Demo_Tool.isabelle_tool)