doc-src/System/Thy/Scala.thy
author wenzelm
Sat, 28 Apr 2012 17:50:42 +0200
changeset 47825 4f25960417ae
child 48602 342ca8f3197b
permissions -rw-r--r--
some coverage of Isabelle/Scala tools;
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
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    17
text {* The Isabelle @{tool_def java} utility is a direct wrapper for
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    18
  the Java Runtime Environment, within the regular Isabelle settings
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
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    41
text {* The Isabelle @{tool_def scala} utility is a direct wrapper for
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    42
  the Scala toplevel; see also @{tool java} above.  The command line
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    43
  arguments are that of the underlying Scala version.
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")
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    49
  scala> isabelle.Isabelle_System.find_logics()
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    50
\end{alltt}
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    51
*}
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
section {* Scala compiler \label{sec:tool-scalac} *}
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    55
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    56
text {* The Isabelle @{tool_def scalac} utility is a direct wrapper
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    57
  for the Scala compiler; see also @{tool scala} above.  The command
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    58
  line arguments are that of the underlying Scala version.
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    59
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    60
  This allows to compile further Scala modules, depending on existing
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    61
  Isabelle/Scala functionality.  The resulting class or jar files can
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    62
  be added to the @{setting CLASSPATH} via the @{verbatim classpath}
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    63
  Bash function that is provided by the Isabelle process environment.
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    64
  Thus add-on components can register themselves in a modular manner,
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    65
  see also \secref{sec:components}.
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    66
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    67
  Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    68
  adding plugin components, which needs special attention since
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    69
  it overrides the standard Java class loader.  *}
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    70
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    71
end