author | wenzelm |
Mon, 04 Aug 2014 17:53:17 +0200 | |
changeset 57855 | 4a5d335a6fc7 |
parent 57320 | 00f2c8d1aa0b |
child 58553 | 3876a1a9ee42 |
permissions | -rw-r--r-- |
47825 | 1 |
theory Scala |
2 |
imports Base |
|
3 |
begin |
|
4 |
||
5 |
chapter {* Isabelle/Scala development tools *} |
|
6 |
||
7 |
text {* Isabelle/ML and Isabelle/Scala are the two main language |
|
8 |
environments for Isabelle tool implementations. There are some basic |
|
9 |
command-line tools to work with the underlying Java Virtual Machine, |
|
10 |
the Scala toplevel and compiler. Note that Isabelle/jEdit |
|
57320
00f2c8d1aa0b
more on command-line invocation -- moved material from system manual;
wenzelm
parents:
53982
diff
changeset
|
11 |
\cite{isabelle-jedit} provides a Scala Console for interactive |
47825 | 12 |
experimentation within the running application. *} |
13 |
||
14 |
||
15 |
section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *} |
|
16 |
||
48602 | 17 |
text {* The @{tool_def java} tool is a direct wrapper for the Java |
18 |
Runtime Environment, within the regular Isabelle settings |
|
47825 | 19 |
environment (\secref{sec:settings}). The command line arguments are |
20 |
that of the underlying Java version. It is run in @{verbatim |
|
21 |
"-server"} mode if possible, to improve performance (at the cost of |
|
22 |
extra startup time). |
|
23 |
||
24 |
The @{verbatim java} executable is the one within @{setting |
|
25 |
ISABELLE_JDK_HOME}, according to the standard directory layout for |
|
26 |
official JDK distributions. The class loader is augmented such that |
|
27 |
the name space of @{verbatim "Isabelle/Pure.jar"} is available, |
|
28 |
which is the main Isabelle/Scala module. |
|
29 |
||
30 |
For example, the following command-line invokes the main method of |
|
31 |
class @{verbatim isabelle.GUI_Setup}, which opens a windows with |
|
32 |
some diagnostic information about the Isabelle environment: |
|
33 |
\begin{alltt} |
|
34 |
isabelle java isabelle.GUI_Setup |
|
35 |
\end{alltt} |
|
36 |
*} |
|
37 |
||
38 |
||
39 |
section {* Scala toplevel \label{sec:tool-scala} *} |
|
40 |
||
48602 | 41 |
text {* The @{tool_def scala} tool is a direct wrapper for the Scala |
42 |
toplevel; see also @{tool java} above. The command line arguments |
|
43 |
are that of the underlying Scala version. |
|
47825 | 44 |
|
45 |
This allows to interact with Isabelle/Scala in TTY mode like this: |
|
46 |
\begin{alltt} |
|
47 |
isabelle scala |
|
48 |
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME") |
|
48815 | 49 |
scala> val options = isabelle.Options.init() |
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 | 52 |
\end{alltt} |
53 |
*} |
|
54 |
||
55 |
||
56 |
section {* Scala compiler \label{sec:tool-scalac} *} |
|
57 |
||
48602 | 58 |
text {* The @{tool_def scalac} tool is a direct wrapper for the Scala |
59 |
compiler; see also @{tool scala} above. The command line arguments |
|
60 |
are that of the underlying Scala version. |
|
47825 | 61 |
|
62 |
This allows to compile further Scala modules, depending on existing |
|
63 |
Isabelle/Scala functionality. The resulting class or jar files can |
|
57855 | 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 | 68 |
|
57320
00f2c8d1aa0b
more on command-line invocation -- moved material from system manual;
wenzelm
parents:
53982
diff
changeset
|
69 |
Note that jEdit \cite{isabelle-jedit} has its own mechanisms for |
47825 | 70 |
adding plugin components, which needs special attention since |
71 |
it overrides the standard Java class loader. *} |
|
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 |
|
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
74 |
section {* Scala script wrapper *} |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
75 |
|
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
76 |
text {* The executable @{executable |
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 | 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 |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
95 |
expanded form. *} |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
96 |
|
47825 | 97 |
end |