diff --git a/src/Doc/System/Environment.thy b/src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy +++ b/src/Doc/System/Environment.thy @@ -1,512 +1,515 @@ (*:maxLineLen=78:*) theory Environment imports Base begin chapter \The Isabelle system environment\ text \ This manual describes Isabelle together with related tools as seen from a system oriented view. See also the \<^emph>\Isabelle/Isar Reference Manual\ @{cite "isabelle-isar-ref"} for the actual Isabelle input language and related concepts, and \<^emph>\The Isabelle/Isar Implementation Manual\ @{cite "isabelle-implementation"} for the main concepts of the underlying implementation in Isabelle/ML. \ section \Isabelle settings \label{sec:settings}\ text \ Isabelle executables may depend on the \<^emph>\Isabelle settings\ within the process environment. This is a statically scoped collection of environment variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}. These variables are \<^emph>\not\ intended to be set directly from the shell, but are provided by Isabelle \<^emph>\components\ their \<^emph>\settings files\ as explained below. \ subsection \Bootstrapping the environment \label{sec:boot}\ text \ Isabelle executables need to be run within a proper settings environment. This is bootstrapped as described below, on the first invocation of one of the outer wrapper scripts (such as @{executable_ref isabelle}). This happens only once for each process tree, i.e.\ the environment is passed to subprocesses according to regular Unix conventions. \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined automatically from the location of the binary that has been run. You should not try to set @{setting ISABELLE_HOME} manually. Also note that the Isabelle executables either have to be run from their original location in the distribution directory, or via the executable objects created by the @{tool install} tool. Symbolic links are admissible, but a plain copy of the \<^dir>\$ISABELLE_HOME/bin\ files will not work! \<^enum> The file \<^file>\$ISABELLE_HOME/etc/settings\ is run as a @{executable_ref bash} shell script with the auto-export option for variables enabled. This file holds a rather long list of shell variable assignments, thus providing the site-wide default settings. The Isabelle distribution already contains a global settings file with sensible defaults for most variables. When installing the system, only a few of these may have to be adapted (probably @{setting ML_SYSTEM} etc.). \<^enum> The file \<^path>\$ISABELLE_HOME_USER/etc/settings\ (if it exists) is run in the same way as the site default settings. Note that the variable @{setting ISABELLE_HOME_USER} has already been set before --- usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2020\. Thus individual users may override the site-wide defaults. Typically, a user settings file contains only a few lines, with some assignments that are actually changed. Never copy the central \<^file>\$ISABELLE_HOME/etc/settings\ file! Since settings files are regular GNU @{executable_def bash} scripts, one may use complex shell commands, such as \<^verbatim>\if\ or \<^verbatim>\case\ statements to set variables depending on the system architecture or other environment variables. Such advanced features should be added only with great care, though. In particular, external environment references should be kept at a minimum. \<^medskip> A few variables are somewhat special, e.g.\ @{setting_def ISABELLE_TOOL} is set automatically to the absolute path name of the @{executable isabelle} executables. \<^medskip> Note that the settings environment may be inspected with the @{tool getenv} tool. This might help to figure out the effect of complex settings scripts. \ subsection \Common variables\ text \ This is a reference of common Isabelle settings variables. Note that the list is somewhat open-ended. Third-party utilities or interfaces may add their own selection. Variables that are special in some sense are marked with \\<^sup>*\. \<^descr>[@{setting_def USER_HOME}\\<^sup>*\] Is the cross-platform user home directory. On Unix systems this is usually the same as @{setting HOME}, but on Windows it is the regular home directory of the user, not the one of within the Cygwin root file-system.\<^footnote>\Cygwin itself offers another choice whether its HOME should point to the \<^path>\/home\ directory tree or the Windows user home.\ \<^descr>[@{setting_def ISABELLE_HOME}\\<^sup>*\] is the location of the top-level Isabelle distribution directory. This is automatically determined from the Isabelle executable that has been invoked. Do not attempt to set @{setting ISABELLE_HOME} yourself from the shell! \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of @{setting ISABELLE_HOME}. The default value is relative to \<^path>\$USER_HOME/.isabelle\, under rare circumstances this may be changed in the global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide defaults may be overridden by a private \<^verbatim>\$ISABELLE_HOME_USER/etc/settings\. \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\\<^sup>*\] is automatically set to the general platform family: \<^verbatim>\linux\, \<^verbatim>\macos\, \<^verbatim>\windows\. Note that platform-dependent tools usually need to refer to the more specific identification according to @{setting ISABELLE_PLATFORM64}, @{setting ISABELLE_PLATFORM32}, @{setting ISABELLE_WINDOWS_PLATFORM64}, @{setting ISABELLE_WINDOWS_PLATFORM32}. \<^descr>[@{setting_def ISABELLE_PLATFORM64}\\<^sup>*\, @{setting_def ISABELLE_PLATFORM32}\\<^sup>*\] indicate the standard Posix platform: \<^verbatim>\x86_64\ for 64 bit and \<^verbatim>\x86\ for 32 bit, together with a symbolic name for the operating system (\<^verbatim>\linux\, \<^verbatim>\darwin\, \<^verbatim>\cygwin\). All platforms support 64 bit executables, some platforms also support 32 bit executables. In GNU bash scripts, it is possible to use the following expressions (with quotes) to specify a preference of 64 bit over 32 bit: @{verbatim [display] \"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\} In contrast, the subsequent expression prefers the old 32 bit variant (which is only relevant for unusual applications): @{verbatim [display] \"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"\} \<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM64}\\<^sup>*\, @{setting_def ISABELLE_WINDOWS_PLATFORM32}\\<^sup>*\] indicate the native Windows platform. These settings are analogous (but independent) of those for the standard Posix subsystem: @{setting ISABELLE_PLATFORM64}, @{setting ISABELLE_PLATFORM32}. In GNU bash scripts, a preference for native Windows platform variants may be specified like this (first 64 bit, second 32 bit): @{verbatim [display] \"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:- ${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"\} \<^descr>[@{setting ISABELLE_TOOL}\\<^sup>*\] is automatically set to the full path name of the @{executable isabelle} executable. \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\\<^sup>*\] refers to the name of this Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2020\''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\\<^sup>*\] specify the underlying ML system to be used for Isabelle. There is only a fixed set of admissable @{setting ML_SYSTEM} names (see the \<^file>\$ISABELLE_HOME/etc/settings\ file of the distribution). The actual compiler binary will be run from the directory @{setting ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line. The optional @{setting ML_PLATFORM} may specify the binary format of ML heap images, which is useful for cross-platform installations. The value of @{setting ML_IDENTIFIER} is automatically obtained by composing the values of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values. \<^descr>[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development Kit) installation with \<^verbatim>\javac\ and \<^verbatim>\jar\ executables. Note that conventional \<^verbatim>\JAVA_HOME\ points to the JRE (Java Runtime Environment), not the JDK. \<^descr>[@{setting_def ISABELLE_JAVA_PLATFORM}] identifies the hardware and operating system platform for the Java installation of Isabelle. That is always the (native) 64 bit variant: \<^verbatim>\x86_64-linux\, \<^verbatim>\x86_64-darwin\, \<^verbatim>\x86_64-windows\. \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where HTML and PDF browser information is stored (see also \secref{sec:info}); its default is \<^path>\$ISABELLE_HOME_USER/browser_info\. For ``system build mode'' (see \secref{sec:tool-build}), @{setting_def ISABELLE_BROWSER_INFO_SYSTEM} is used instead; its default is \<^path>\$ISABELLE_HOME/browser_info\. \<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images, log files, and build databases are stored; its default is \<^path>\$ISABELLE_HOME_USER/heaps\. If @{system_option system_heaps} is \<^verbatim>\true\, @{setting_def ISABELLE_HEAPS_SYSTEM} is used instead; its default is \<^path>\$ISABELLE_HOME/heaps\. See also \secref{sec:tool-build}. \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none is given explicitely by the user. The default value is \<^verbatim>\HOL\. \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the @{tool_ref console} interface. \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle document preparation (see also \secref{sec:tool-latex}). \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories that are scanned by @{executable isabelle} for external utility programs (see also \secref{sec:isabelle-tool}). \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories with documentation files. \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying \<^verbatim>\pdf\ files. \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying \<^verbatim>\dvi\ files. \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\\<^sup>*\] is the prefix from which any running Isabelle ML process derives an individual directory for temporary files. \<^descr>[@{setting_def ISABELLE_TOOL_JAVA_OPTIONS}] is passed to the \<^verbatim>\java\ executable when running Isabelle tools (e.g.\ @{tool build}). This is occasionally helpful to provide more heap space, via additional options like \<^verbatim>\-Xms1g -Xmx4g\. \ subsection \Additional components \label{sec:components}\ text \ Any directory may be registered as an explicit \<^emph>\Isabelle component\. The general layout conventions are that of the main Isabelle distribution itself, and the following two files (both optional) have a special meaning: \<^item> \<^verbatim>\etc/settings\ holds additional settings that are initialized when bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As usual, the content is interpreted as a GNU bash script. It may refer to the component's enclosing directory via the \<^verbatim>\COMPONENT\ shell variable. For example, the following setting allows to refer to files within the component later on, without having to hardwire absolute paths: @{verbatim [display] \MY_COMPONENT_HOME="$COMPONENT"\} Components can also add to existing Isabelle settings such as @{setting_def ISABELLE_TOOLS}, in order to provide component-specific tools that can be invoked by end-users. For example: @{verbatim [display] \ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\} \<^item> \<^verbatim>\etc/components\ holds a list of further sub-components of the same structure. The directory specifications given here can be either absolute (with leading \<^verbatim>\/\) or relative to the component's main directory. The root of component initialization is @{setting ISABELLE_HOME} itself. After initializing all of its sub-components recursively, @{setting ISABELLE_HOME_USER} is included in the same manner (if that directory exists). This allows to install private components via \<^path>\$ISABELLE_HOME_USER/etc/components\, although it is often more convenient to do that programmatically via the \<^bash_function>\init_component\ shell function in the \<^verbatim>\etc/settings\ script of \<^verbatim>\$ISABELLE_HOME_USER\ (or any other component directory). For example: @{verbatim [display] \init_component "$HOME/screwdriver-2.0"\} This is tolerant wrt.\ missing component directories, but might produce a warning. \<^medskip> More complex situations may be addressed by initializing components listed in a given catalog file, relatively to some base directory: @{verbatim [display] \init_components "$HOME/my_component_store" "some_catalog_file"\} The component directories listed in the catalog file are treated as relative to the given base directory. See also \secref{sec:tool-components} for some tool-support for resolving components that are formally initialized but not installed yet. \ section \The Isabelle tool wrapper \label{sec:isabelle-tool}\ text \ The main \<^emph>\Isabelle tool wrapper\ provides a generic startup environment for Isabelle-related utilities, user interfaces, add-on applications etc. Such tools automatically benefit from the settings mechanism (\secref{sec:settings}). Moreover, this is the standard way to invoke Isabelle/Scala functionality as a separate operating-system process. Isabelle command-line tools are run uniformly via a common wrapper --- @{executable_ref isabelle}: @{verbatim [display] \Usage: isabelle TOOL [ARGS ...] Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. Available tools: ...\} Tools may be implemented in Isabelle/Scala or as stand-alone executables (usually as GNU bash scripts). In the invocation of ``@{executable isabelle}~\tool\'', the named \tool\ is resolved as follows (and in the given order). \<^enum> An external tool found on the directories listed in the @{setting ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX notation). \<^enum> If a file ``\tool\\<^verbatim>\.scala\'' is found, the source needs to define some object that extends the class \<^verbatim>\Isabelle_Tool.Body\. The Scala compiler is invoked on the spot (which may take some time), and the body function is run with the command-line arguments as \<^verbatim>\List[String]\. \<^enum> If an executable file ``\tool\'' is found, it is invoked as stand-alone program with the command-line arguments provided as \<^verbatim>\argv\ array. - \<^enum> An internal tool that is registered in \<^verbatim>\Isabelle_Tool.internal_tools\ - within the Isabelle/Scala namespace of \<^verbatim>\Pure.jar\. This is the preferred - entry-point for high-end tools implemented in Isabelle/Scala --- compiled - once when the Isabelle distribution is built. These tools are provided by - Isabelle/Pure and cannot be augmented in user-space. + \<^enum> An internal tool that is registered in \<^verbatim>\etc/settings\ via the shell + function \<^bash_function>\isabelle_scala_service\, referring to a + suitable instance of class \<^scala_type>\isabelle.Isabelle_Scala_Tools\. + This is the preferred approach for non-trivial systems programming in + Isabelle/Scala: instead of adhoc interpretation of \<^verbatim>\scala\ scripts, + which is somewhat slow and only type-checked at runtime, there are + properly compiled \<^verbatim>\jar\ modules (see also the shell function + \<^bash_function>\classpath\ in \secref{sec:scala}). - There are also some administrative tools that are available from a bare + There are also various administrative tools that are available from a bare repository clone of Isabelle, but not in regular distributions. \ subsubsection \Examples\ text \ Show the list of available documentation of the Isabelle distribution: @{verbatim [display] \isabelle doc\} View a certain document as follows: @{verbatim [display] \isabelle doc system\} Query the Isabelle settings environment: @{verbatim [display] \isabelle getenv ISABELLE_HOME_USER\} \ section \The raw Isabelle ML process\ subsection \Batch mode \label{sec:tool-process}\ text \ The @{tool_def process} tool runs the raw ML process in batch mode: @{verbatim [display] \Usage: isabelle process [OPTIONS] Options are: -T THEORY load theory -d DIR include session directory -e ML_EXPR evaluate ML expression on startup -f ML_FILE evaluate ML file on startup -l NAME logic session name (default ISABELLE_LOGIC="HOL") -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Run the raw Isabelle ML process in batch mode.\} \<^medskip> Options \<^verbatim>\-e\ and \<^verbatim>\-f\ allow to evaluate ML code, before the ML process is started. The source is either given literally or taken from a file. Multiple \<^verbatim>\-e\ and \<^verbatim>\-f\ options are evaluated in the given order. Errors lead to premature exit of the ML process with return code 1. \<^medskip> Option \<^verbatim>\-T\ loads a specified theory file. This is a wrapper for \<^verbatim>\-e\ with a suitable \<^ML>\use_thy\ invocation. \<^medskip> Option \<^verbatim>\-l\ specifies the logic session name. Option \<^verbatim>\-d\ specifies additional directories for session roots, see also \secref{sec:tool-build}. \<^medskip> The \<^verbatim>\-m\ option adds identifiers of print modes to be made active for this session. For example, \<^verbatim>\-m ASCII\ prefers ASCII replacement syntax over mathematical Isabelle symbols. \<^medskip> Option \<^verbatim>\-o\ allows to override Isabelle system options for this process, see also \secref{sec:system-options}. \ subsubsection \Examples\ text \ The subsequent example retrieves the \<^verbatim>\Main\ theory value from the theory loader within ML: @{verbatim [display] \isabelle process -e 'Thy_Info.get_theory "Main"'\} Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The Isabelle/ML and Scala libraries provide functions for that, but here we need to do it manually. \<^medskip> This is how to invoke a function body with proper return code and printing of errors, and without printing of a redundant \<^verbatim>\val it = (): unit\ result: @{verbatim [display] \isabelle process -e 'Command_Line.tool (fn () => writeln "OK")'\} @{verbatim [display] \isabelle process -e 'Command_Line.tool (fn () => error "Bad")'\} \ subsection \Interactive mode\ text \ The @{tool_def console} tool runs the raw ML process with interactive console and line editor: @{verbatim [display] \Usage: isabelle console [OPTIONS] Options are: -d DIR include session directory -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC) -m MODE add print mode for output -n no build of session image on startup -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r bootstrap from raw Poly/ML Build a logic session image and run the raw Isabelle ML process in interactive mode, with line editor ISABELLE_LINE_EDITOR.\} \<^medskip> Option \<^verbatim>\-l\ specifies the logic session name. By default, its heap image is checked and built on demand, but the option \<^verbatim>\-n\ skips that. Option \<^verbatim>\-i\ includes additional sessions into the name-space of theories: multiple occurrences are possible. Option \<^verbatim>\-r\ indicates a bootstrap from the raw Poly/ML system, which is relevant for Isabelle/Pure development. \<^medskip> Options \<^verbatim>\-d\, \<^verbatim>\-m\, \<^verbatim>\-o\ have the same meaning as for @{tool process} (\secref{sec:tool-process}). \<^medskip> The Isabelle/ML process is run through the line editor that is specified via the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\ @{executable_def rlwrap} for GNU readline); the fall-back is to use plain standard input/output. The user is connected to the raw ML toplevel loop: this is neither Isabelle/Isar nor Isabelle/ML within the usual formal context. The most relevant ML commands at this stage are \<^ML>\use\ (for ML files) and \<^ML>\use_thy\ (for theory files). \ section \The raw Isabelle Java process \label{sec:isabelle-java}\ text \ The @{executable_ref isabelle_java} executable allows to run a Java process within the name space of Java and Scala components that are bundled with Isabelle, but \<^emph>\without\ the Isabelle settings environment (\secref{sec:settings}). After such a JVM cold-start, the Isabelle environment can be accessed via \<^verbatim>\Isabelle_System.getenv\ as usual, but the underlying process environment remains clean. This is e.g.\ relevant when invoking other processes that should remain separate from the current Isabelle installation. \<^medskip> Note that under normal circumstances, Isabelle command-line tools are run \<^emph>\within\ the settings environment, as provided by the @{executable isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}). \ subsubsection \Example\ text \ The subsequent example creates a raw Java process on the command-line and invokes the main Isabelle application entry point: @{verbatim [display] \isabelle_java isabelle.Main\} \ section \YXML versus XML \label{sec:yxml-vs-xml}\ text \ Isabelle tools often use YXML, which is a simple and efficient syntax for untyped XML trees. The YXML format is defined as follows. \<^enum> The encoding is always UTF-8. \<^enum> Body text is represented verbatim (no escaping, no special treatment of white space, no named entities, no CDATA chunks, no comments). \<^enum> Markup elements are represented via ASCII control characters \\<^bold>X = 5\ and \\<^bold>Y = 6\ as follows: \begin{tabular}{ll} XML & YXML \\\hline \<^verbatim>\<\\name attribute\\<^verbatim>\=\\value \\\<^verbatim>\>\ & \\<^bold>X\<^bold>Yname\<^bold>Yattribute\\<^verbatim>\=\\value\\<^bold>X\ \\ \<^verbatim>\\name\\<^verbatim>\>\ & \\<^bold>X\<^bold>Y\<^bold>X\ \\ \end{tabular} There is no special case for empty body text, i.e.\ \<^verbatim>\\ is treated like \<^verbatim>\\. Also note that \\<^bold>X\ and \\<^bold>Y\ may never occur in well-formed XML documents. Parsing YXML is pretty straight-forward: split the text into chunks separated by \\<^bold>X\, then split each chunk into sub-chunks separated by \\<^bold>Y\. Markup chunks start with an empty sub-chunk, and a second empty sub-chunk indicates close of an element. Any other non-empty chunk consists of plain text. For example, see \<^file>\~~/src/Pure/PIDE/yxml.ML\ or \<^file>\~~/src/Pure/PIDE/yxml.scala\. YXML documents may be detected quickly by checking that the first two characters are \\<^bold>X\<^bold>Y\. \ end diff --git a/src/Doc/System/Scala.thy b/src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy +++ b/src/Doc/System/Scala.thy @@ -1,336 +1,336 @@ (*:maxLineLen=78:*) theory Scala imports Base begin -chapter \Isabelle/Scala systems programming\ +chapter \Isabelle/Scala systems programming \label{sec:scala}\ text \ Isabelle/ML and Isabelle/Scala are the two main implementation languages of the Isabelle environment: \<^item> Isabelle/ML is for \<^emph>\mathematics\, to develop tools within the context of symbolic logic, e.g.\ for constructing proofs or defining domain-specific formal languages. See the \<^emph>\Isabelle/Isar implementation manual\ @{cite "isabelle-implementation"} for more details. \<^item> Isabelle/Scala is for \<^emph>\physics\, to connect with the world of systems and services, including editors and IDE frameworks. There are various ways to access Isabelle/Scala modules and operations: \<^item> Isabelle command-line tools (\secref{sec:scala-tools}) run in a separate Java process. \<^item> Isabelle/ML antiquotations access Isabelle/Scala functions (\secref{sec:scala-functions}) via the PIDE protocol: execution happens within the running Java process underlying Isabelle/Scala. \<^item> The \<^verbatim>\Console/Scala\ plugin of Isabelle/jEdit @{cite "isabelle-jedit"} operates on the running Java application, using the Scala read-eval-print-loop (REPL). The main Isabelle/Scala functionality is provided by \<^verbatim>\Pure.jar\, 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>\etc/settings\ shell script in the component directory. Some shell functions are available to help with that: \<^item> Function \<^bash_function>\classpath\ adds \<^verbatim>\jar\ 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}). \<^item> Function \<^bash_function>\isabelle_scala_service\ registers global service providers as subclasses of \<^scala_type>\isabelle.Isabelle_System.Service\, 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>\$\ to be interpreted by the shell). Particular Isabelle/Scala services require particular subclasses: instances are filtered according to their dynamic type. For example, class \<^scala_type>\isabelle.Isabelle_Scala_Tools\ collects Scala command-line tools, and class \<^scala_type>\isabelle.Scala.Functions\ collects Scala functions (\secref{sec:scala-functions}). \ section \Command-line tools \label{sec:scala-tools}\ subsection \Java Runtime Environment \label{sec:tool-java}\ text \ The @{tool_def java} tool is a direct wrapper for the Java Runtime Environment, within the regular Isabelle settings environment (\secref{sec:settings}) and Isabelle classpath. The command line arguments are that of the bundled Java distribution: see option \<^verbatim>\-help\ in particular. The \<^verbatim>\java\ executable is taken from @{setting ISABELLE_JDK_HOME}, according to the standard directory layout for regular distributions of OpenJDK. The shell function \<^bash_function>\isabelle_jdk\ allows shell scripts to invoke other Java tools robustly (e.g.\ \<^verbatim>\isabelle_jdk jar\), without depending on accidental operating system installations. \ subsection \Scala toplevel \label{sec:tool-scala}\ text \ The @{tool_def scala} tool is a direct wrapper for the Scala toplevel, similar to @{tool java} above. The command line arguments are that of the bundled Scala distribution: see option \<^verbatim>\-help\ in particular. This allows to interact with Isabelle/Scala interactively. \ subsubsection \Example\ text \ Explore the Isabelle system environment in Scala: @{verbatim [display, indent = 2] \$ isabelle scala\} @{scala [display, indent = 2] \import isabelle._ val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME") val options = Options.init() options.bool("browser_info") options.string("document")\} \ subsection \Scala compiler \label{sec:tool-scalac}\ text \ 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>\class\ or \<^verbatim>\jar\ files can be added to the Java classpath using the shell function \<^bash_function>\classpath\. 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. \ subsection \Scala script wrapper\ text \ The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run Isabelle/Scala source files stand-alone programs, by using a suitable ``hash-bang'' line and executable file permissions. For example: @{verbatim [display, indent = 2] \#!/usr/bin/env isabelle_scala_script\} @{scala [display, indent = 2] \val options = isabelle.Options.init() Console.println("browser_info = " + options.bool("browser_info")) Console.println("document = " + options.string("document"))\} This assumes that the executable may be found via the @{setting PATH} from the process environment: this is the case when Isabelle settings are active, e.g.\ in the context of the main Isabelle tool wrapper \secref{sec:isabelle-tool}. Alternatively, the full \<^file>\$ISABELLE_HOME/bin/isabelle_scala_script\ may be specified in expanded form. \ subsection \Project setup for common Scala IDEs\ text \ The @{tool_def scala_project} tool creates a project configuration for Isabelle/Scala/jEdit: @{verbatim [display] \Usage: isabelle scala_project [OPTIONS] PROJECT_DIR Options are: -L make symlinks to original scala files Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs such as IntelliJ IDEA.\} The generated configuration is for Gradle\<^footnote>\\<^url>\https://gradle.org\\, but the main purpose is to import it into common Scala IDEs, such as IntelliJ IDEA\<^footnote>\\<^url>\https://www.jetbrains.com/idea\\. This allows to explore the sources with static analysis and other hints in real-time. The specified project directory needs to be fresh. The generated files refer to physical file-system locations, using the path notation of the underlying OS platform. Thus the project needs to be recreated whenever the Isabelle installation is changed or moved. \<^medskip> By default, Scala sources are \<^emph>\copied\ from the Isabelle distribution and editing them within the IDE has no permanent effect. Option \<^verbatim>\-L\ produces \<^emph>\symlinks\ to the original files: this allows to develop Isabelle/Scala/jEdit within an external Scala IDE. Note that building the result always requires \<^verbatim>\isabelle jedit -b\ on the command-line. \ section \Registered Isabelle/Scala functions \label{sec:scala-functions}\ subsection \Defining functions in Isabelle/Scala\ text \ A Scala functions of type \<^scala_type>\String => String\ may be wrapped as \<^scala_type>\isabelle.Scala.Fun\ and collected via an instance of the class \<^scala_type>\isabelle.Scala.Functions\. A system component can then register that class via \<^bash_function>\isabelle_scala_service\ in \<^path>\etc/settings\ (\secref{sec:components}). An example is the predefined collection of \<^scala_type>\isabelle.Scala.Functions\ in Isabelle/\<^verbatim>\Pure.jar\ with the following line in \<^file>\$ISABELLE_HOME/etc/settings\: @{verbatim [display, indent = 2] \isabelle_scala_service 'isabelle.Functions'\} The overall list of registered functions is accessible in Isabelle/Scala as \<^scala_object>\isabelle.Scala.functions\. \ subsection \Invoking functions in Isabelle/ML\ text \ Isabelle/PIDE provides a protocol to invoke registered Scala functions in ML: this works both within the Prover IDE and in batch builds. The subsequent ML antiquotations refer to Scala functions in a formally-checked manner. \begin{matharray}{rcl} @{ML_antiquotation_def "scala_function"} & : & \ML_antiquotation\ \\ @{ML_antiquotation_def "scala"} & : & \ML_antiquotation\ \\ \end{matharray} \<^rail>\ (@{ML_antiquotation scala_function} | @{ML_antiquotation scala}) @{syntax embedded} \ \<^descr> \@{scala_function name}\ inlines the checked function name as ML string literal. \<^descr> \@{scala name}\ invokes the checked function via the PIDE protocol. In Isabelle/ML this appears as a function of type \<^ML_type>\string -> string\, which is subject to interrupts within the ML runtime environment as usual. A \<^scala>\null\ result in Scala raises an exception \<^ML>\Scala.Null\ in ML. The standard approach of representing datatypes via strings works via XML in YXML transfer syntax. See Isabelle/ML operations and modules @{ML YXML.string_of_body}, @{ML YXML.parse_body}, @{ML_structure XML.Encode}, @{ML_structure XML.Decode}; similarly for Isabelle/Scala. Isabelle symbols may have to be recoded via Scala operations \<^scala_method>\isabelle.Symbol.decode\ and \<^scala_method>\isabelle.Symbol.encode\. \ subsubsection \Examples\ text \ Invoke a predefined Scala function that is the identity on type \<^ML_type>\string\: \ ML \ val s = "test"; val s' = \<^scala>\echo\ s; \<^assert> (s = s') \ text \ Let the Scala compiler process some toplevel declarations, producing a list of errors: \ ML \ val source = "class A(a: Int, b: Boolean)" val errors = \<^scala>\scala_toplevel\ source |> YXML.parse_body |> let open XML.Decode in list string end; \<^assert> (null errors)\ text \ The above is merely for demonstration. See \<^ML>\Scala_Compiler.toplevel\ for a more convenient version with builtin decoding and treatment of errors. \ section \Documenting Isabelle/Scala entities\ text \ The subsequent document antiquotations help to document Isabelle/Scala entities, with formal checking of names against the Isabelle classpath. \begin{matharray}{rcl} @{antiquotation_def "scala"} & : & \antiquotation\ \\ @{antiquotation_def "scala_object"} & : & \antiquotation\ \\ @{antiquotation_def "scala_type"} & : & \antiquotation\ \\ @{antiquotation_def "scala_method"} & : & \antiquotation\ \\ \end{matharray} \<^rail>\ (@@{antiquotation scala} | @@{antiquotation scala_object}) @{syntax embedded} ; @@{antiquotation scala_type} @{syntax embedded} types ; @@{antiquotation scala_method} class @{syntax embedded} types args ; class: ('(' @'in' @{syntax name} types ')')? ; types: ('[' (@{syntax name} ',' +) ']')? ; args: ('(' (nat | (('_' | @{syntax name}) + ',')) ')')? \ \<^descr> \@{scala s}\ is similar to \@{verbatim s}\, but the given source text is checked by the Scala compiler as toplevel declaration (without evaluation). This allows to write Isabelle/Scala examples that are statically checked. \<^descr> \@{scala_object x}\ checks the given Scala object name (simple value or ground module) and prints the result verbatim. \<^descr> \@{scala_type T[A]}\ checks the given Scala type name (with optional type parameters) and prints the result verbatim. \<^descr> \@{scala_method (in c[A]) m[B](n)}\ checks the given Scala method \m\ in the context of class \c\. The method argument slots are either specified by a number \n\ or by a list of (optional) argument types; this may refer to type variables specified for the class or method: \A\ or \B\ above. Everything except for the method name \m\ is optional. The absence of the class context means that this is a static method. The absence of arguments with types means that the method can be determined uniquely as \<^verbatim>\(\\m\\<^verbatim>\ _)\ in Scala (no overloading). \ subsubsection \Examples\ text \ Miscellaneous Isabelle/Scala entities: \<^item> object: \<^scala_object>\isabelle.Isabelle_Process\ \<^item> type without parameter: @{scala_type isabelle.Console_Progress} \<^item> type with parameter: @{scala_type List[A]} \<^item> static method: \<^scala_method>\isabelle.Isabelle_System.bash\ \<^item> class and method with type parameters: @{scala_method (in List[A]) map[B]("A => B")} \<^item> overloaded method with argument type: @{scala_method (in Int) "+" (Int)} \ end