Theory Scala

(*:maxLineLen=78:*)

theory Scala
imports Base
begin

chapter ‹Isabelle/Scala development tools›

text ‹
  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.
›


section ‹Java Runtime Environment within Isabelle \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}). The command line arguments are that of the
  underlying Java version. It is run in ▩‹-server› mode if possible, to
  improve performance (at the cost of extra startup time).

  The ▩‹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
  ▩‹Isabelle/Pure.jar› is available, which is the main Isabelle/Scala module.

  For example, the following command-line invokes the main method of class
  ▩‹isabelle.GUI_Setup›, which opens a windows with some diagnostic
  information about the Isabelle environment:
  @{verbatim [display] ‹isabelle java isabelle.GUI_Setup›}
›


section ‹Scala toplevel \label{sec:tool-scala}›

text ‹
  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:
  @{verbatim [display]
‹isabelle scala
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
scala> val options = isabelle.Options.init()
scala> options.bool("browser_info")
scala> options.string("document")›}
›


section ‹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
  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 ▩‹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.
›


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

  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"}):
  @{verbatim [display]
‹#!/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"))›}

  Alternatively the full @{file "$ISABELLE_HOME/bin/isabelle_scala_script"}
  may be specified in expanded form.
›

end