--- 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>.