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: