wenzelm@48696
|
1 |
theory Scala
|
wenzelm@48696
|
2 |
imports Base
|
wenzelm@48696
|
3 |
begin
|
wenzelm@48696
|
4 |
|
wenzelm@48696
|
5 |
chapter {* Isabelle/Scala development tools *}
|
wenzelm@48696
|
6 |
|
wenzelm@48696
|
7 |
text {* Isabelle/ML and Isabelle/Scala are the two main language
|
wenzelm@48696
|
8 |
environments for Isabelle tool implementations. There are some basic
|
wenzelm@48696
|
9 |
command-line tools to work with the underlying Java Virtual Machine,
|
wenzelm@48696
|
10 |
the Scala toplevel and compiler. Note that Isabelle/jEdit
|
wenzelm@58662
|
11 |
\cite{isabelle-jedit} provides a Scala Console for interactive
|
wenzelm@48696
|
12 |
experimentation within the running application. *}
|
wenzelm@48696
|
13 |
|
wenzelm@48696
|
14 |
|
wenzelm@48696
|
15 |
section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *}
|
wenzelm@48696
|
16 |
|
wenzelm@49617
|
17 |
text {* The @{tool_def java} tool is a direct wrapper for the Java
|
wenzelm@49617
|
18 |
Runtime Environment, within the regular Isabelle settings
|
wenzelm@48696
|
19 |
environment (\secref{sec:settings}). The command line arguments are
|
wenzelm@48696
|
20 |
that of the underlying Java version. It is run in @{verbatim
|
wenzelm@48696
|
21 |
"-server"} mode if possible, to improve performance (at the cost of
|
wenzelm@48696
|
22 |
extra startup time).
|
wenzelm@48696
|
23 |
|
wenzelm@48696
|
24 |
The @{verbatim java} executable is the one within @{setting
|
wenzelm@48696
|
25 |
ISABELLE_JDK_HOME}, according to the standard directory layout for
|
wenzelm@48696
|
26 |
official JDK distributions. The class loader is augmented such that
|
wenzelm@48696
|
27 |
the name space of @{verbatim "Isabelle/Pure.jar"} is available,
|
wenzelm@48696
|
28 |
which is the main Isabelle/Scala module.
|
wenzelm@48696
|
29 |
|
wenzelm@48696
|
30 |
For example, the following command-line invokes the main method of
|
wenzelm@48696
|
31 |
class @{verbatim isabelle.GUI_Setup}, which opens a windows with
|
wenzelm@48696
|
32 |
some diagnostic information about the Isabelle environment:
|
wenzelm@48696
|
33 |
\begin{alltt}
|
wenzelm@48696
|
34 |
isabelle java isabelle.GUI_Setup
|
wenzelm@48696
|
35 |
\end{alltt}
|
wenzelm@48696
|
36 |
*}
|
wenzelm@48696
|
37 |
|
wenzelm@48696
|
38 |
|
wenzelm@48696
|
39 |
section {* Scala toplevel \label{sec:tool-scala} *}
|
wenzelm@48696
|
40 |
|
wenzelm@49617
|
41 |
text {* The @{tool_def scala} tool is a direct wrapper for the Scala
|
wenzelm@49617
|
42 |
toplevel; see also @{tool java} above. The command line arguments
|
wenzelm@49617
|
43 |
are that of the underlying Scala version.
|
wenzelm@48696
|
44 |
|
wenzelm@48696
|
45 |
This allows to interact with Isabelle/Scala in TTY mode like this:
|
wenzelm@48696
|
46 |
\begin{alltt}
|
wenzelm@48696
|
47 |
isabelle scala
|
wenzelm@48696
|
48 |
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
|
wenzelm@49830
|
49 |
scala> val options = isabelle.Options.init()
|
wenzelm@49830
|
50 |
scala> options.bool("browser_info")
|
wenzelm@53253
|
51 |
scala> options.string("document")
|
wenzelm@48696
|
52 |
\end{alltt}
|
wenzelm@48696
|
53 |
*}
|
wenzelm@48696
|
54 |
|
wenzelm@48696
|
55 |
|
wenzelm@48696
|
56 |
section {* Scala compiler \label{sec:tool-scalac} *}
|
wenzelm@48696
|
57 |
|
wenzelm@49617
|
58 |
text {* The @{tool_def scalac} tool is a direct wrapper for the Scala
|
wenzelm@49617
|
59 |
compiler; see also @{tool scala} above. The command line arguments
|
wenzelm@49617
|
60 |
are that of the underlying Scala version.
|
wenzelm@48696
|
61 |
|
wenzelm@48696
|
62 |
This allows to compile further Scala modules, depending on existing
|
wenzelm@48696
|
63 |
Isabelle/Scala functionality. The resulting class or jar files can
|
wenzelm@59071
|
64 |
be added to the Java classpath using the @{verbatim classpath} Bash
|
wenzelm@54713
|
65 |
function that is provided by the Isabelle process environment. Thus
|
wenzelm@54713
|
66 |
add-on components can register themselves in a modular manner, see
|
wenzelm@54713
|
67 |
also \secref{sec:components}.
|
wenzelm@48696
|
68 |
|
wenzelm@58662
|
69 |
Note that jEdit \cite{isabelle-jedit} has its own mechanisms for
|
wenzelm@48696
|
70 |
adding plugin components, which needs special attention since
|
wenzelm@48696
|
71 |
it overrides the standard Java class loader. *}
|
wenzelm@48696
|
72 |
|
wenzelm@53253
|
73 |
|
wenzelm@53253
|
74 |
section {* Scala script wrapper *}
|
wenzelm@53253
|
75 |
|
wenzelm@53253
|
76 |
text {* The executable @{executable
|
wenzelm@53253
|
77 |
"$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run
|
wenzelm@53253
|
78 |
Isabelle/Scala source files stand-alone programs, by using a
|
wenzelm@53253
|
79 |
suitable ``hash-bang'' line and executable file permissions.
|
wenzelm@53253
|
80 |
|
wenzelm@53253
|
81 |
The subsequent example assumes that the main Isabelle binaries have
|
wenzelm@53253
|
82 |
been installed in some directory that is included in @{setting PATH}
|
wenzelm@53253
|
83 |
(see also @{tool "install"}):
|
wenzelm@53253
|
84 |
|
wenzelm@53253
|
85 |
\begin{alltt}
|
wenzelm@53253
|
86 |
#!/usr/bin/env isabelle_scala_script
|
wenzelm@53253
|
87 |
|
wenzelm@53253
|
88 |
val options = isabelle.Options.init()
|
wenzelm@53253
|
89 |
Console.println("browser_info = " + options.bool("browser_info"))
|
wenzelm@53253
|
90 |
Console.println("document = " + options.string("document"))
|
wenzelm@53253
|
91 |
\end{alltt}
|
wenzelm@53253
|
92 |
|
wenzelm@55119
|
93 |
Alternatively the full @{file
|
wenzelm@53253
|
94 |
"$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
|
wenzelm@53253
|
95 |
expanded form. *}
|
wenzelm@53253
|
96 |
|
wenzelm@48696
|
97 |
end
|