theory Scala
imports Base
begin
chapter \<open>Isabelle/Scala development tools\<close>
text \<open>Isabelle/ML and Isabelle/Scala are the two main language
environments for Isabelle tool implementations. There are some basic
command-line tools to work with the underlying Java Virtual Machine,
the Scala toplevel and compiler. Note that Isabelle/jEdit
@{cite "isabelle-jedit"} provides a Scala Console for interactive
experimentation within the running application.\<close>
section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
text \<open>The @{tool_def java} tool is a direct wrapper for the Java
Runtime Environment, within the regular Isabelle settings
environment (\secref{sec:settings}). The command line arguments are
that of the underlying Java version. It is run in @{verbatim
"-server"} mode if possible, to improve performance (at the cost of
extra startup time).
The @{verbatim java} executable is the one within @{setting
ISABELLE_JDK_HOME}, according to the standard directory layout for
official JDK distributions. The class loader is augmented such that
the name space of @{verbatim "Isabelle/Pure.jar"} is available,
which is the main Isabelle/Scala module.
For example, the following command-line invokes the main method of
class @{verbatim isabelle.GUI_Setup}, which opens a windows with
some diagnostic information about the Isabelle environment:
\begin{alltt}
isabelle java isabelle.GUI_Setup
\end{alltt}
\<close>
section \<open>Scala toplevel \label{sec:tool-scala}\<close>
text \<open>The @{tool_def scala} tool is a direct wrapper for the Scala
toplevel; see also @{tool java} above. The command line arguments
are that of the underlying Scala version.
This allows to interact with Isabelle/Scala in TTY mode like this:
\begin{alltt}
isabelle scala
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
scala> val options = isabelle.Options.init()
scala> options.bool("browser_info")
scala> options.string("document")
\end{alltt}
\<close>
section \<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 underlying Scala version.
This allows to compile further Scala modules, depending on existing
Isabelle/Scala functionality. The resulting class or jar files can
be added to the Java classpath using the @{verbatim classpath} Bash
function that is provided by the Isabelle process environment. Thus
add-on components can register themselves in a modular manner, see
also \secref{sec:components}.
Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for
adding plugin components, which needs special attention since
it overrides the standard Java class loader.\<close>
section \<open>Scala script wrapper\<close>
text \<open>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.
The subsequent example assumes that the main Isabelle binaries have
been installed in some directory that is included in @{setting PATH}
(see also @{tool "install"}):
\begin{alltt}
#!/usr/bin/env isabelle_scala_script
val options = isabelle.Options.init()
Console.println("browser_info = " + options.bool("browser_info"))
Console.println("document = " + options.string("document"))
\end{alltt}
Alternatively the full @{file
"$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
expanded form.\<close>
end