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