# HG changeset patch
# User wenzelm
# Date 1626637576 -7200
# Node ID 6bf9f94198a77dbc0a7211863ac425bd85dc6be7
# Parent  aa36845ad5ade22ad6cb4d09ddf03d61ef9817e5
updated documentation on Isabelle/Scala;

diff -r aa36845ad5ad -r 6bf9f94198a7 lib/Tools/scala_build
--- a/lib/Tools/scala_build	Sun Jul 18 13:41:20 2021 +0200
+++ b/lib/Tools/scala_build	Sun Jul 18 21:46:16 2021 +0200
@@ -17,6 +17,9 @@
   echo "    -f           force fresh build"
   echo "    -q           quiet mode: suppress stdout/stderr"
   echo
+  echo "  Build Isabelle/Scala/Java modules of all registered components"
+  echo "  (if required)."
+  echo
   exit 1
 }
 
diff -r aa36845ad5ad -r 6bf9f94198a7 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Sun Jul 18 13:41:20 2021 +0200
+++ b/src/Doc/System/Scala.thy	Sun Jul 18 21:46:16 2021 +0200
@@ -31,30 +31,22 @@
     operates on the running Java application, using the Scala
     read-eval-print-loop (REPL).
 
-  The main Isabelle/Scala functionality is provided by \<^verbatim>\<open>isabelle.jar\<close>, but
-  further add-ons are bundled with Isabelle, e.g.\ to access SQLite or
-  PostgreSQL using JDBC (Java Database Connectivity).
-
-  Other components may augment the system environment by providing a suitable
-  \<^path>\<open>etc/settings\<close> shell script in the component directory. Some shell
-  functions are available to help with that:
-
-    \<^item> Function \<^bash_function>\<open>classpath\<close> adds \<^verbatim>\<open>jar\<close> files in Isabelle path
-    notation (POSIX). On Windows, this is converted to native path names
-    before invoking @{tool java} or @{tool scala} (\secref{sec:scala-tools}).
+  The main Isabelle/Scala/jEdit functionality is provided by
+  \<^file>\<open>$ISABELLE_HOME/lib/classes/isabelle.jar\<close>. Further underlying Scala and
+  Java libraries are bundled with Isabelle, e.g.\ to access SQLite or
+  PostgreSQL via JDBC.
 
-    \<^item> Function \<^bash_function>\<open>isabelle_scala_service\<close> registers global
-    service providers as subclasses of
-    \<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>, using the raw Java name
-    according to @{scala_method (in java.lang.Object) getClass} (it should be
-    enclosed in single quotes to avoid special characters like \<^verbatim>\<open>$\<close> to be
-    interpreted by the shell).
+  Add-on Isabelle components may augment the system environment by providing
+  suitable configuration in \<^path>\<open>etc/settings\<close> (GNU bash script). The
+  shell function \<^bash_function>\<open>classpath\<close> helps to write
+  \<^path>\<open>etc/settings\<close> in a portable manner: it refers to library \<^verbatim>\<open>jar\<close>
+  files in standard POSIX path notation. On Windows, this is converted to
+  native platform format, before invoking Java (\secref{sec:scala-tools}).
 
-    Particular Isabelle/Scala services require particular subclasses:
-    instances are filtered according to their dynamic type. For example, class
-    \<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close> collects Scala command-line
-    tools, and class \<^scala_type>\<open>isabelle.Scala.Functions\<close>
-    collects Scala functions (\secref{sec:scala-functions}).
+  \<^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}).
 \<close>
 
 
@@ -103,25 +95,6 @@
 \<close>
 
 
-subsection \<open>Scala compiler \label{sec:tool-scalac}\<close>
-
-text \<open>
-  The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
-  also @{tool scala} above. The command line arguments are that of the
-  bundled Scala distribution.
-
-  This allows to compile further Scala modules, depending on existing
-  Isabelle/Scala functionality. The resulting \<^verbatim>\<open>class\<close> or \<^verbatim>\<open>jar\<close> files can be
-  added to the Java classpath using the shell function
-  \<^bash_function>\<open>classpath\<close>. Thus add-on components can register themselves
-  in a modular manner, see also \secref{sec:components}.
-
-  Note that Isabelle/jEdit @{cite "isabelle-jedit"} has its own mechanisms for
-  adding plugin components. This needs special attention, since it overrides
-  the standard Java class loader.
-\<close>
-
-
 subsection \<open>Scala script wrapper\<close>
 
 text \<open>
@@ -143,11 +116,156 @@
 \<close>
 
 
-subsection \<open>Project setup for common Scala IDEs\<close>
+subsection \<open>Scala compiler \label{sec:tool-scalac}\<close>
+
+text \<open>
+  The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
+  also @{tool scala} above. The command line arguments are that of the
+  bundled Scala distribution.
+
+  This provides a low-level mechanism to compile further Scala modules,
+  depending on existing Isabelle/Scala functionality; the resulting \<^verbatim>\<open>class\<close>
+  or \<^verbatim>\<open>jar\<close> files can be added to the Java classpath using the shell function
+  \<^bash_function>\<open>classpath\<close>.
+
+  A more convenient high-level approach works via \<^path>\<open>etc/build.props\<close>
+  (see \secref{sec:scala-build}).
+\<close>
+
+
+section \<open>Isabelle/Scala/Java modules \label{sec:scala-build}\<close>
+
+subsection \<open>Component configuration via \<^path>\<open>etc/build.props\<close>\<close>
 
 text \<open>
-  The @{tool_def scala_project} tool creates a project configuration for
-  Isabelle/Scala/jEdit:
+  Isabelle components may augment the Isabelle/Scala/Java environment
+  declaratively via properties given in \<^path>\<open>etc/build.props\<close> (within the
+  component directory). This specifies an output \<^verbatim>\<open>jar\<close> \<^emph>\<open>module\<close>, based on
+  Scala or Java \<^emph>\<open>sources\<close>, and arbitrary \<^emph>\<open>resources\<close>. Moreover, a module can
+  specify \<^emph>\<open>services\<close> that are subclasses of
+  \<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>; these have a particular
+  meaning to Isabelle/Scala tools.
+
+  Before running a Scala or Java process, the Isabelle system implicitly
+  ensures that all provided modules are compiled and packaged (as jars). It is
+  also possible to invoke @{tool scala_build} explicitly, with extra options.
+
+  \<^medskip>
+  The syntax of in \<^path>\<open>etc/build.props\<close> follows a regular Java properties
+  file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/15/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
+  but the encoding is \<^verbatim>\<open>UTF-8\<close>, instead of historic \<^verbatim>\<open>ISO 8859-1\<close> from the API
+  documentation.
+
+  The subsequent properties are relevant for the Scala/Java build process.
+  Most properties are optional: the default is an empty string (or list). File
+  names are relative to the main component directory and may refer to Isabelle
+  settings variables (e.g. \<^verbatim>\<open>$ISABELLE_HOME\<close>).
+
+    \<^item> \<^verbatim>\<open>title\<close> (required) is a human-readable description of the module, used
+    in printed messages.
+
+    \<^item> \<^verbatim>\<open>module\<close> specifies a \<^verbatim>\<open>jar\<close> file name for the output module, as result
+    of compiling the specified sources (and resources). If this is absent,
+    there is no build process, but contributing sources may still be given,
+    possibly together with \<^verbatim>\<open>no_module\<close> as described below.
+
+    \<^item> \<^verbatim>\<open>no_module\<close> means that there is no build process, but the specified
+    \<^verbatim>\<open>jar\<close> is provided by other means. This is relevant for @{tool
+    scala_project} (\secref{sec:tool-scala-project}), which includes all
+    Scala/Java sources of components, but suppresses \<^verbatim>\<open>jar\<close> modules to avoid
+    duplication of content.
+
+    \<^item> \<^verbatim>\<open>scalac_options\<close> and \<^verbatim>\<open>javac_options\<close> augment the default settings
+    @{setting_ref ISABELLE_SCALAC_OPTIONS} and @{setting_ref
+    ISABELLE_JAVAC_OPTIONS} for this component; option syntax follows the
+    regular command-line tools \<^verbatim>\<open>scalac\<close> and \<^verbatim>\<open>javac\<close>, respectively.
+
+    \<^item> \<^verbatim>\<open>main\<close> specifies the main entry point for the \<^verbatim>\<open>jar\<close> module. This is
+    only relevant for direct invocation like ``\<^verbatim>\<open>java -jar test.jar\<close>''.
+
+    \<^item> \<^verbatim>\<open>requirements\<close> is a list of \<^verbatim>\<open>jar\<close> modules that are needed in the
+    compilation process, but not provided by the regular classpath (notably
+    @{setting ISABELLE_CLASSPATH}).
+
+    A \emph{normal entry} refers to a single \<^verbatim>\<open>jar\<close> file name, possibly with
+    settings variables as usual. E.g. \<^file>\<open>$ISABELLE_SCALA_JAR\<close> for the main
+    \<^file>\<open>$ISABELLE_HOME/lib/classes/isabelle.jar\<close> (especially relevant for
+    add-on modules).
+
+    A \emph{special entry} is of of the form \<^verbatim>\<open>env:\<close>\<open>variable\<close> and refers to a
+    settings variable from the Isabelle environment: its value may consist of
+    multiple \<^verbatim>\<open>jar\<close> entries (separated by colons). Environment variables are
+    not expanded recursively.
+
+    \<^item> \<^verbatim>\<open>resources\<close> is a list of files that should be included in the resulting
+    \<^verbatim>\<open>jar\<close> file. Each item consists of a pair separated by colon:
+    \<open>source\<close>\<^verbatim>\<open>:\<close>\<open>target\<close> means to copy an existing source file (relative to
+    the component directory) to the given target file or directory (relative
+    to the \<^verbatim>\<open>jar\<close> name space). A \<open>file\<close> specification without colon
+    abbreviates \<open>file\<close>\<^verbatim>\<open>:\<close>\<open>file\<close>, i.e. the file is copied while retaining its
+    relative path name.
+
+    \<^item> \<^verbatim>\<open>sources\<close> is a list of \<^verbatim>\<open>.scala\<close> or \<^verbatim>\<open>.java\<close> files that contribute to
+    the specified module. It is possible to use both languages simultaneously:
+    the Scala and Java compiler will be invoked consecutively to make this
+    work.
+
+    \<^item> \<^verbatim>\<open>services\<close> is a list of class names to be registered as Isabelle
+    service providers (subclasses of
+    \<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>). Internal class names of
+    the underlying JVM need to be given: e.g. see method @{scala_method (in
+    java.lang.Object) getClass}.
+
+    Particular services require particular subclasses: instances are filtered
+    according to their dynamic type. For example, class
+    \<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close> collects Scala command-line
+    tools, and class \<^scala_type>\<open>isabelle.Scala.Functions\<close> collects Scala
+    functions (\secref{sec:scala-functions}).
+\<close>
+
+
+subsection \<open>Explicit Isabelle/Scala/Java build \label{sec:tool-scala-build}\<close>
+
+text \<open>
+  The @{tool_def scala_build} tool explicitly invokes the build process for
+  all registered components.
+  @{verbatim [display]
+\<open>Usage: isabelle scala_build [OPTIONS]
+
+  Options are:
+    -f           force fresh build
+    -q           quiet mode: suppress stdout/stderr
+
+  Build Isabelle/Scala/Java modules of all registered components
+  (if required).
+\<close>}
+
+  For each registered Isabelle component that provides
+  \<^path>\<open>etc/build.props\<close>, the specified output \<^verbatim>\<open>module\<close> is checked against
+  the corresponding input \<^verbatim>\<open>requirements\<close>, \<^verbatim>\<open>resources\<close>, \<^verbatim>\<open>sources\<close>. If
+  required, there is an automatic build using \<^verbatim>\<open>scalac\<close> or \<^verbatim>\<open>javac\<close> (or both).
+  The identity of input files is recorded within the output \<^verbatim>\<open>jar\<close>, using SHA1
+  digests in \<^verbatim>\<open>META-INF/isabelle/shasum\<close>.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-f\<close> forces a fresh build, regardless of the up-to-date status of
+  input files vs. the output module.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-q\<close> suppresses all output on stdout/stderr produced by the Scala or
+  Java compiler.
+
+  \<^medskip> Explicit invocation of \<^verbatim>\<open>isabelle scala_build\<close> mainly serves testing or
+  applications with special options: the Isabelle system normally does an
+  automatic the build on demand.
+\<close>
+
+
+subsection \<open>Project setup for common Scala IDEs \label{sec:tool-scala-project}\<close>
+
+text \<open>
+  The @{tool_def scala_project} tool creates a project configuration for all
+  Isabelle/Scala/Java modules specified in components via \<^path>\<open>etc/build.props\<close>:
   @{verbatim [display]
 \<open>Usage: isabelle scala_project [OPTIONS] PROJECT_DIR
 
@@ -172,9 +290,9 @@
   editing them within the IDE has no permanent effect.
 
   Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
-  develop Isabelle/Scala/jEdit within an external Scala IDE. Note that
-  building the result always requires \<^verbatim>\<open>isabelle jedit -b\<close> on the
-  command-line.
+  develop Isabelle/Scala/jEdit within an external Scala IDE. Note that the
+  result cannot be built within the IDE: it requires implicit or explicit
+  \<^verbatim>\<open>isabelle scala_build\<close> (\secref{sec:tool-scala-build}).
 \<close>
 
 
@@ -185,13 +303,10 @@
 text \<open>
   A Scala functions of type \<^scala_type>\<open>String => String\<close> may be wrapped as
   \<^scala_type>\<open>isabelle.Scala.Fun\<close> and collected via an instance of the
-  class \<^scala_type>\<open>isabelle.Scala.Functions\<close>. A system component
-  can then register that class via \<^bash_function>\<open>isabelle_scala_service\<close>
-  in \<^path>\<open>etc/settings\<close> (\secref{sec:components}). An example is the
-  predefined collection of \<^scala_type>\<open>isabelle.Scala.Functions\<close> in
-  \<^verbatim>\<open>isabelle.jar\<close> with the following line in
-  \<^file>\<open>$ISABELLE_HOME/etc/settings\<close>:
-  @{verbatim [display, indent = 2] \<open>isabelle_scala_service 'isabelle.Functions'\<close>}
+  class \<^scala_type>\<open>isabelle.Scala.Functions\<close>. A system component can then
+  register that class via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>
+  (\secref{sec:scala-build}). An example is the predefined collection of
+  \<^scala_type>\<open>isabelle.Scala.Functions\<close> in \<^file>\<open>$ISABELLE_HOME/etc/build.props\<close>.
 
   The overall list of registered functions is accessible in Isabelle/Scala as
   \<^scala_object>\<open>isabelle.Scala.functions\<close>.