|
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 Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for |
|
41 the Java 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 Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for |
|
66 the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above. The command line |
|
67 arguments 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> isabelle.Isabelle_System.find_logics() |
|
74 \end{alltt}% |
|
75 \end{isamarkuptext}% |
|
76 \isamarkuptrue% |
|
77 % |
|
78 \isamarkupsection{Scala compiler \label{sec:tool-scalac}% |
|
79 } |
|
80 \isamarkuptrue% |
|
81 % |
|
82 \begin{isamarkuptext}% |
|
83 The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper |
|
84 for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above. The command |
|
85 line arguments are that of the underlying Scala version. |
|
86 |
|
87 This allows to compile further Scala modules, depending on existing |
|
88 Isabelle/Scala functionality. The resulting class or jar files can |
|
89 be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath| |
|
90 Bash function that is provided by the Isabelle process environment. |
|
91 Thus add-on components can register themselves in a modular manner, |
|
92 see also \secref{sec:components}. |
|
93 |
|
94 Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for |
|
95 adding plugin components, which needs special attention since |
|
96 it overrides the standard Java class loader.% |
|
97 \end{isamarkuptext}% |
|
98 \isamarkuptrue% |
|
99 % |
|
100 \isadelimtheory |
|
101 % |
|
102 \endisadelimtheory |
|
103 % |
|
104 \isatagtheory |
|
105 \isacommand{end}\isamarkupfalse% |
|
106 % |
|
107 \endisatagtheory |
|
108 {\isafoldtheory}% |
|
109 % |
|
110 \isadelimtheory |
|
111 % |
|
112 \endisadelimtheory |
|
113 \isanewline |
|
114 \end{isabellebody}% |
|
115 %%% Local Variables: |
|
116 %%% mode: latex |
|
117 %%% TeX-master: "root" |
|
118 %%% End: |