1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Scala}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Scala\isanewline |
|
12 \isakeyword{imports}\ Base\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupchapter{Isabelle/Scala development tools% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \begin{isamarkuptext}% |
|
26 Isabelle/ML and Isabelle/Scala are the two main language |
|
27 environments for Isabelle tool implementations. There are some basic |
|
28 command-line tools to work with the underlying Java Virtual Machine, |
|
29 the Scala toplevel and compiler. Note that Isabelle/jEdit |
|
30 (\secref{sec:tool-tty}) provides a Scala Console for interactive |
|
31 experimentation within the running application.% |
|
32 \end{isamarkuptext}% |
|
33 \isamarkuptrue% |
|
34 % |
|
35 \isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}% |
|
36 } |
|
37 \isamarkuptrue% |
|
38 % |
|
39 \begin{isamarkuptext}% |
|
40 The \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatool{java}}}}} tool is a direct wrapper for the Java |
|
41 Runtime Environment, within the regular Isabelle settings |
|
42 environment (\secref{sec:settings}). The command line arguments are |
|
43 that of the underlying Java version. It is run in \verb|-server| mode if possible, to improve performance (at the cost of |
|
44 extra startup time). |
|
45 |
|
46 The \verb|java| executable is the one within \hyperlink{setting.ISABELLE-JDK-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}JDK{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, according to the standard directory layout for |
|
47 official JDK distributions. The class loader is augmented such that |
|
48 the name space of \verb|Isabelle/Pure.jar| is available, |
|
49 which is the main Isabelle/Scala module. |
|
50 |
|
51 For example, the following command-line invokes the main method of |
|
52 class \verb|isabelle.GUI_Setup|, which opens a windows with |
|
53 some diagnostic information about the Isabelle environment: |
|
54 \begin{alltt} |
|
55 isabelle java isabelle.GUI_Setup |
|
56 \end{alltt}% |
|
57 \end{isamarkuptext}% |
|
58 \isamarkuptrue% |
|
59 % |
|
60 \isamarkupsection{Scala toplevel \label{sec:tool-scala}% |
|
61 } |
|
62 \isamarkuptrue% |
|
63 % |
|
64 \begin{isamarkuptext}% |
|
65 The \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatool{scala}}}}} tool is a direct wrapper for the Scala |
|
66 toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatool{java}}}} above. The command line arguments |
|
67 are that of the underlying Scala version. |
|
68 |
|
69 This allows to interact with Isabelle/Scala in TTY mode like this: |
|
70 \begin{alltt} |
|
71 isabelle scala |
|
72 scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME") |
|
73 scala> val options = isabelle.Options.init() |
|
74 scala> options.bool("browser_info") |
|
75 \end{alltt}% |
|
76 \end{isamarkuptext}% |
|
77 \isamarkuptrue% |
|
78 % |
|
79 \isamarkupsection{Scala compiler \label{sec:tool-scalac}% |
|
80 } |
|
81 \isamarkuptrue% |
|
82 % |
|
83 \begin{isamarkuptext}% |
|
84 The \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatool{scalac}}}}} tool is a direct wrapper for the Scala |
|
85 compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatool{scala}}}} above. The command line arguments |
|
86 are that of the underlying Scala version. |
|
87 |
|
88 This allows to compile further Scala modules, depending on existing |
|
89 Isabelle/Scala functionality. The resulting class or jar files can |
|
90 be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath| |
|
91 Bash function that is provided by the Isabelle process environment. |
|
92 Thus add-on components can register themselves in a modular manner, |
|
93 see also \secref{sec:components}. |
|
94 |
|
95 Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for |
|
96 adding plugin components, which needs special attention since |
|
97 it overrides the standard Java class loader.% |
|
98 \end{isamarkuptext}% |
|
99 \isamarkuptrue% |
|
100 % |
|
101 \isadelimtheory |
|
102 % |
|
103 \endisadelimtheory |
|
104 % |
|
105 \isatagtheory |
|
106 \isacommand{end}\isamarkupfalse% |
|
107 % |
|
108 \endisatagtheory |
|
109 {\isafoldtheory}% |
|
110 % |
|
111 \isadelimtheory |
|
112 % |
|
113 \endisadelimtheory |
|
114 \isanewline |
|
115 \end{isabellebody}% |
|
116 %%% Local Variables: |
|
117 %%% mode: latex |
|
118 %%% TeX-master: "root" |
|
119 %%% End: |
|