src/Doc/System/Scala.thy
author wenzelm
Tue, 31 Mar 2015 22:31:05 +0200
changeset 59886 e0dc738eb08c
parent 58618 782f0b662cae
child 61407 7ba7b8103565
permissions -rw-r--r--
support for explicit scope of private entries;
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
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
     5
chapter \<open>Isabelle/Scala development tools\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
     7
text \<open>Isabelle/ML and Isabelle/Scala are the two main language
47825
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
58553
3876a1a9ee42 prefer @{cite} antiquotation;
wenzelm
parents: 57855
diff changeset
    11
@{cite "isabelle-jedit"} provides a Scala Console for interactive
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    12
experimentation within the running application.\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    13
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    14
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    15
section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    16
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    17
text \<open>The @{tool_def java} tool is a direct wrapper for the Java
48602
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}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    36
\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    37
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    38
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    39
section \<open>Scala toplevel \label{sec:tool-scala}\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    40
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    41
text \<open>The @{tool_def scala} tool is a direct wrapper for the Scala
48602
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")
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    51
  scala> options.string("document")
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    52
\end{alltt}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    53
\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    54
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    55
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    56
section \<open>Scala compiler \label{sec:tool-scalac}\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    57
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    58
text \<open>The @{tool_def scalac} tool is a direct wrapper for the Scala
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 47825
diff changeset
    59
  compiler; see also @{tool scala} above.  The command line arguments
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 47825
diff changeset
    60
  are that of the underlying Scala version.
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    61
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    62
  This allows to compile further Scala modules, depending on existing
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    63
  Isabelle/Scala functionality.  The resulting class or jar files can
57855
wenzelm
parents: 57320
diff changeset
    64
  be added to the Java classpath using the @{verbatim classpath} Bash
53576
793a429c63e7 maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents: 52116
diff changeset
    65
  function that is provided by the Isabelle process environment.  Thus
793a429c63e7 maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents: 52116
diff changeset
    66
  add-on components can register themselves in a modular manner, see
793a429c63e7 maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents: 52116
diff changeset
    67
  also \secref{sec:components}.
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    68
58553
3876a1a9ee42 prefer @{cite} antiquotation;
wenzelm
parents: 57855
diff changeset
    69
  Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    70
  adding plugin components, which needs special attention since
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    71
  it overrides the standard Java class loader.\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    72
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    73
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    74
section \<open>Scala script wrapper\<close>
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    75
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    76
text \<open>The executable @{executable
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    77
  "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    78
  Isabelle/Scala source files stand-alone programs, by using a
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    79
  suitable ``hash-bang'' line and executable file permissions.
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    80
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    81
  The subsequent example assumes that the main Isabelle binaries have
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    82
  been installed in some directory that is included in @{setting PATH}
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    83
  (see also @{tool "install"}):
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    84
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    85
\begin{alltt}
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    86
#!/usr/bin/env isabelle_scala_script
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    87
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    88
val options = isabelle.Options.init()
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    89
Console.println("browser_info = " + options.bool("browser_info"))
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    90
Console.println("document = " + options.string("document"))
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    91
\end{alltt}
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    92
53982
wenzelm
parents: 53576
diff changeset
    93
  Alternatively the full @{file
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    94
  "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    95
  expanded form.\<close>
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    96
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    97
end