doc-src/System/Scala.thy
changeset 48937 e7418f8d49fe
parent 48815 eed6698b2ba0
equal deleted inserted replaced
48936:e6d9e46ff7bc 48937:e7418f8d49fe
       
     1 theory Scala
       
     2 imports Base
       
     3 begin
       
     4 
       
     5 chapter {* Isabelle/Scala development tools *}
       
     6 
       
     7 text {* Isabelle/ML and Isabelle/Scala are the two main language
       
     8 environments for Isabelle tool implementations.  There are some basic
       
     9 command-line tools to work with the underlying Java Virtual Machine,
       
    10 the Scala toplevel and compiler.  Note that Isabelle/jEdit
       
    11 (\secref{sec:tool-tty}) provides a Scala Console for interactive
       
    12 experimentation within the running application. *}
       
    13 
       
    14 
       
    15 section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *}
       
    16 
       
    17 text {* The @{tool_def java} tool is a direct wrapper for the Java
       
    18   Runtime Environment, within the regular Isabelle settings
       
    19   environment (\secref{sec:settings}).  The command line arguments are
       
    20   that of the underlying Java version.  It is run in @{verbatim
       
    21   "-server"} mode if possible, to improve performance (at the cost of
       
    22   extra startup time).
       
    23 
       
    24   The @{verbatim java} executable is the one within @{setting
       
    25   ISABELLE_JDK_HOME}, according to the standard directory layout for
       
    26   official JDK distributions.  The class loader is augmented such that
       
    27   the name space of @{verbatim "Isabelle/Pure.jar"} is available,
       
    28   which is the main Isabelle/Scala module.
       
    29 
       
    30   For example, the following command-line invokes the main method of
       
    31   class @{verbatim isabelle.GUI_Setup}, which opens a windows with
       
    32   some diagnostic information about the Isabelle environment:
       
    33 \begin{alltt}
       
    34   isabelle java isabelle.GUI_Setup
       
    35 \end{alltt}
       
    36 *}
       
    37 
       
    38 
       
    39 section {* Scala toplevel \label{sec:tool-scala} *}
       
    40 
       
    41 text {* The @{tool_def scala} tool is a direct wrapper for the Scala
       
    42   toplevel; see also @{tool java} above.  The command line arguments
       
    43   are that of the underlying Scala version.
       
    44 
       
    45   This allows to interact with Isabelle/Scala in TTY mode like this:
       
    46 \begin{alltt}
       
    47   isabelle scala
       
    48   scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
       
    49   scala> val options = isabelle.Options.init()
       
    50   scala> options.bool("browser_info")
       
    51 \end{alltt}
       
    52 *}
       
    53 
       
    54 
       
    55 section {* Scala compiler \label{sec:tool-scalac} *}
       
    56 
       
    57 text {* The @{tool_def scalac} tool is a direct wrapper for the Scala
       
    58   compiler; see also @{tool scala} above.  The command line arguments
       
    59   are that of the underlying Scala version.
       
    60 
       
    61   This allows to compile further Scala modules, depending on existing
       
    62   Isabelle/Scala functionality.  The resulting class or jar files can
       
    63   be added to the @{setting CLASSPATH} via the @{verbatim classpath}
       
    64   Bash function that is provided by the Isabelle process environment.
       
    65   Thus add-on components can register themselves in a modular manner,
       
    66   see also \secref{sec:components}.
       
    67 
       
    68   Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
       
    69   adding plugin components, which needs special attention since
       
    70   it overrides the standard Java class loader.  *}
       
    71 
       
    72 end