src/Doc/System/Scala.thy
author wenzelm
Sat, 10 Jun 2017 21:48:02 +0200
changeset 66061 880db47fed30
parent 63680 6e1e8b5abbfa
child 71378 820cf124dced
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61656
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61575
diff changeset
     1
(*:maxLineLen=78:*)
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
     2
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
     3
theory Scala
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
     4
imports Base
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
     5
begin
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
     7
chapter \<open>Isabelle/Scala development tools\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
     8
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
     9
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    10
  Isabelle/ML and Isabelle/Scala are the two main language environments for
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    11
  Isabelle tool implementations. There are some basic command-line tools to
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    12
  work with the underlying Java Virtual Machine, the Scala toplevel and
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    13
  compiler. Note that Isabelle/jEdit @{cite "isabelle-jedit"} provides a Scala
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    14
  Console for interactive experimentation within the running application.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    15
\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    16
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    17
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    18
section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    19
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    20
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    21
  The @{tool_def java} tool is a direct wrapper for the Java Runtime
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    22
  Environment, within the regular Isabelle settings environment
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    23
  (\secref{sec:settings}). The command line arguments are that of the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    24
  underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode if possible, to
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    25
  improve performance (at the cost of extra startup time).
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    26
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    27
  The \<^verbatim>\<open>java\<close> executable is the one within @{setting ISABELLE_JDK_HOME},
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    28
  according to the standard directory layout for official JDK distributions.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    29
  The class loader is augmented such that the name space of
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    30
  \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available, which is the main Isabelle/Scala module.
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    31
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    32
  For example, the following command-line invokes the main method of class
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    33
  \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with some diagnostic
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    34
  information about the Isabelle environment:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    35
  @{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
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
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    41
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    42
  The @{tool_def scala} tool is a direct wrapper for the Scala toplevel; see
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    43
  also @{tool java} above. The command line arguments are that of the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    44
  underlying Scala version.
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    45
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    46
  This allows to interact with Isabelle/Scala in TTY mode like this:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    47
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    48
\<open>isabelle scala
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    49
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    50
scala> val options = isabelle.Options.init()
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    51
scala> options.bool("browser_info")
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    52
scala> options.string("document")\<close>}
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
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    58
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    59
  The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    60
  also @{tool scala} above. The command line arguments are that of the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    61
  underlying Scala version.
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    62
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    63
  This allows to compile further Scala modules, depending on existing
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    64
  Isabelle/Scala functionality. The resulting class or jar files can be added
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    65
  to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash function that is provided
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    66
  by the Isabelle process environment. Thus add-on components can register
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    67
  themselves in a modular manner, see also \secref{sec:components}.
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    68
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    69
  Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    70
  plugin components, which needs special attention since it overrides the
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    71
  standard Java class loader.
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    72
\<close>
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    73
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    74
58618
782f0b662cae more cartouches;
wenzelm
parents: 58553
diff changeset
    75
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
    76
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    77
text \<open>
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    78
  The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    79
  allows to run Isabelle/Scala source files stand-alone programs, by using a
62415
62c03eb38e49 isabelle_scala_script is usually found by PATH;
wenzelm
parents: 61656
diff changeset
    80
  suitable ``hash-bang'' line and executable file permissions. For example:
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    81
  @{verbatim [display]
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    82
\<open>#!/usr/bin/env isabelle_scala_script
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    83
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    84
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
    85
Console.println("browser_info = " + options.bool("browser_info"))
61407
7ba7b8103565 @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 58618
diff changeset
    86
Console.println("document = " + options.string("document"))\<close>}
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    87
62415
62c03eb38e49 isabelle_scala_script is usually found by PATH;
wenzelm
parents: 61656
diff changeset
    88
  This assumes that the executable may be found via the @{setting PATH} from
62c03eb38e49 isabelle_scala_script is usually found by PATH;
wenzelm
parents: 61656
diff changeset
    89
  the process environment: this is the case when Isabelle settings are active,
62c03eb38e49 isabelle_scala_script is usually found by PATH;
wenzelm
parents: 61656
diff changeset
    90
  e.g.\ in the context of the main Isabelle tool wrapper
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 62415
diff changeset
    91
  \secref{sec:isabelle-tool}. Alternatively, the full
6e1e8b5abbfa more symbols;
wenzelm
parents: 62415
diff changeset
    92
  \<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
62415
62c03eb38e49 isabelle_scala_script is usually found by PATH;
wenzelm
parents: 61656
diff changeset
    93
  form.
61575
f18f6e51e901 tuned whitespace;
wenzelm
parents: 61503
diff changeset
    94
\<close>
52116
abf9fcfa65cf added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents: 48985
diff changeset
    95
47825
4f25960417ae some coverage of Isabelle/Scala tools;
wenzelm
parents:
diff changeset
    96
end