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