doc-src/System/Thy/document/Scala.tex
 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 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Scala}%

     4 %

     5 \isadelimtheory

     6 %

     7 \endisadelimtheory

     8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ Scala\isanewline

    12 \isakeyword{imports}\ Base\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

    21 \isamarkupchapter{Isabelle/Scala development tools%

    22 }

    23 \isamarkuptrue%

    24 %

    25 \begin{isamarkuptext}%

    26 Isabelle/ML and Isabelle/Scala are the two main language

    27 environments for Isabelle tool implementations.  There are some basic

    28 command-line tools to work with the underlying Java Virtual Machine,

    29 the Scala toplevel and compiler.  Note that Isabelle/jEdit

    30 (\secref{sec:tool-tty}) provides a Scala Console for interactive

    31 experimentation within the running application.%

    32 \end{isamarkuptext}%

    33 \isamarkuptrue%

    34 %

    35 \isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}%

    36 }

    37 \isamarkuptrue%

    38 %

    39 \begin{isamarkuptext}%

    40 The Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for

    41   the Java Runtime Environment, within the regular Isabelle settings

    42   environment (\secref{sec:settings}).  The command line arguments are

    43   that of the underlying Java version.  It is run in \verb|-server| mode if possible, to improve performance (at the cost of

    44   extra startup time).

    45

    46   The \verb|java| executable is the one within \hyperlink{setting.ISABELLE-JDK-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}JDK{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, according to the standard directory layout for

    47   official JDK distributions.  The class loader is augmented such that

    48   the name space of \verb|Isabelle/Pure.jar| is available,

    49   which is the main Isabelle/Scala module.

    50

    51   For example, the following command-line invokes the main method of

    52   class \verb|isabelle.GUI_Setup|, which opens a windows with

    53   some diagnostic information about the Isabelle environment:

    54 \begin{alltt}

    55   isabelle java isabelle.GUI_Setup

    56 \end{alltt}%

    57 \end{isamarkuptext}%

    58 \isamarkuptrue%

    59 %

    60 \isamarkupsection{Scala toplevel \label{sec:tool-scala}%

    61 }

    62 \isamarkuptrue%

    63 %

    64 \begin{isamarkuptext}%

    65 The Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for

    66   the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above.  The command line

    67   arguments are that of the underlying Scala version.

    68

    69   This allows to interact with Isabelle/Scala in TTY mode like this:

    70 \begin{alltt}

    71   isabelle scala

    72   scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")

    73   scala> isabelle.Isabelle_System.find_logics()

    74 \end{alltt}%

    75 \end{isamarkuptext}%

    76 \isamarkuptrue%

    77 %

    78 \isamarkupsection{Scala compiler \label{sec:tool-scalac}%

    79 }

    80 \isamarkuptrue%

    81 %

    82 \begin{isamarkuptext}%

    83 The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper

    84   for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above.  The command

    85   line arguments are that of the underlying Scala version.

    86

    87   This allows to compile further Scala modules, depending on existing

    88   Isabelle/Scala functionality.  The resulting class or jar files can

    89   be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath|

    90   Bash function that is provided by the Isabelle process environment.

    91   Thus add-on components can register themselves in a modular manner,

    92   see also \secref{sec:components}.

    93

    94   Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for

    95   adding plugin components, which needs special attention since

    96   it overrides the standard Java class loader.%

    97 \end{isamarkuptext}%

    98 \isamarkuptrue%

    99 %

   100 \isadelimtheory

   101 %

   102 \endisadelimtheory

   103 %

   104 \isatagtheory

   105 \isacommand{end}\isamarkupfalse%

   106 %

   107 \endisatagtheory

   108 {\isafoldtheory}%

   109 %

   110 \isadelimtheory

   111 %

   112 \endisadelimtheory

   113 \isanewline

   114 \end{isabellebody}%

   115 %%% Local Variables:

   116 %%% mode: latex

   117 %%% TeX-master: "root"

   118 %%% End: