# HG changeset patch
# User wenzelm
# Date 1700925188 -3600
# Node ID f13390b2c1ee10d01d8ba247ba1a0fe6c483d135
# Parent  156bfa6a28369f0284c42da2fc142376c09fc43d
provide src/Tools/Demo as example for system component with Isabelle/Scala tool;

diff -r 156bfa6a2836 -r f13390b2c1ee NEWS
--- 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
diff -r 156bfa6a2836 -r f13390b2c1ee etc/components
--- 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
diff -r 156bfa6a2836 -r f13390b2c1ee src/Doc/System/Scala.thy
--- 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>
 
 
diff -r 156bfa6a2836 -r f13390b2c1ee src/Tools/Demo/README.md
--- /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).
diff -r 156bfa6a2836 -r f13390b2c1ee src/Tools/Demo/etc/build.props
--- /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
diff -r 156bfa6a2836 -r f13390b2c1ee src/Tools/Demo/etc/options
--- /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"
diff -r 156bfa6a2836 -r f13390b2c1ee src/Tools/Demo/etc/settings
--- /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"
diff -r 156bfa6a2836 -r f13390b2c1ee src/Tools/Demo/src/demo_tool.scala
--- /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)