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