doc-src/System/Thy/Scala.thy
author wenzelm
Sat Apr 28 17:50:42 2012 +0200 (2012-04-28)
changeset 47825 4f25960417ae
child 48602 342ca8f3197b
permissions -rw-r--r--
some coverage of Isabelle/Scala tools;
     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 Isabelle @{tool_def java} utility is a direct wrapper for
    18   the Java 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 Isabelle @{tool_def scala} utility is a direct wrapper for
    42   the Scala toplevel; see also @{tool java} above.  The command line
    43   arguments 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> isabelle.Isabelle_System.find_logics()
    50 \end{alltt}
    51 *}
    52 
    53 
    54 section {* Scala compiler \label{sec:tool-scalac} *}
    55 
    56 text {* The Isabelle @{tool_def scalac} utility is a direct wrapper
    57   for the Scala compiler; see also @{tool scala} above.  The command
    58   line arguments are that of the underlying Scala version.
    59 
    60   This allows to compile further Scala modules, depending on existing
    61   Isabelle/Scala functionality.  The resulting class or jar files can
    62   be added to the @{setting CLASSPATH} via the @{verbatim classpath}
    63   Bash function that is provided by the Isabelle process environment.
    64   Thus add-on components can register themselves in a modular manner,
    65   see also \secref{sec:components}.
    66 
    67   Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
    68   adding plugin components, which needs special attention since
    69   it overrides the standard Java class loader.  *}
    70 
    71 end