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