author | wenzelm |
Sun, 27 Feb 2022 20:00:23 +0100 | |
changeset 75161 | 95612f330c93 |
parent 74960 | f03ece7155d6 |
child 75688 | 598994a2d339 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
47825 | 3 |
theory Scala |
4 |
imports Base |
|
5 |
begin |
|
6 |
||
72252 | 7 |
chapter \<open>Isabelle/Scala systems programming \label{sec:scala}\<close> |
47825 | 8 |
|
61575 | 9 |
text \<open> |
71907 | 10 |
Isabelle/ML and Isabelle/Scala are the two main implementation languages of |
11 |
the Isabelle environment: |
|
12 |
||
13 |
\<^item> Isabelle/ML is for \<^emph>\<open>mathematics\<close>, to develop tools within the context |
|
14 |
of symbolic logic, e.g.\ for constructing proofs or defining |
|
15 |
domain-specific formal languages. See the \<^emph>\<open>Isabelle/Isar implementation |
|
16 |
manual\<close> @{cite "isabelle-implementation"} for more details. |
|
17 |
||
18 |
\<^item> Isabelle/Scala is for \<^emph>\<open>physics\<close>, to connect with the world of systems |
|
19 |
and services, including editors and IDE frameworks. |
|
20 |
||
21 |
There are various ways to access Isabelle/Scala modules and operations: |
|
22 |
||
23 |
\<^item> Isabelle command-line tools (\secref{sec:scala-tools}) run in a separate |
|
24 |
Java process. |
|
25 |
||
26 |
\<^item> Isabelle/ML antiquotations access Isabelle/Scala functions |
|
27 |
(\secref{sec:scala-functions}) via the PIDE protocol: execution happens |
|
28 |
within the running Java process underlying Isabelle/Scala. |
|
29 |
||
30 |
\<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit @{cite "isabelle-jedit"} |
|
31 |
operates on the running Java application, using the Scala |
|
32 |
read-eval-print-loop (REPL). |
|
33 |
||
74041 | 34 |
The main Isabelle/Scala/jEdit functionality is provided by |
35 |
\<^file>\<open>$ISABELLE_HOME/lib/classes/isabelle.jar\<close>. Further underlying Scala and |
|
36 |
Java libraries are bundled with Isabelle, e.g.\ to access SQLite or |
|
37 |
PostgreSQL via JDBC. |
|
71907 | 38 |
|
74041 | 39 |
Add-on Isabelle components may augment the system environment by providing |
40 |
suitable configuration in \<^path>\<open>etc/settings\<close> (GNU bash script). The |
|
41 |
shell function \<^bash_function>\<open>classpath\<close> helps to write |
|
42 |
\<^path>\<open>etc/settings\<close> in a portable manner: it refers to library \<^verbatim>\<open>jar\<close> |
|
43 |
files in standard POSIX path notation. On Windows, this is converted to |
|
44 |
native platform format, before invoking Java (\secref{sec:scala-tools}). |
|
71907 | 45 |
|
74041 | 46 |
\<^medskip> |
47 |
There is also an implicit build process for Isabelle/Scala/Java modules, |
|
48 |
based on \<^path>\<open>etc/build.props\<close> within the component directory (see also |
|
49 |
\secref{sec:scala-build}). |
|
61575 | 50 |
\<close> |
47825 | 51 |
|
52 |
||
71907 | 53 |
section \<open>Command-line tools \label{sec:scala-tools}\<close> |
54 |
||
55 |
subsection \<open>Java Runtime Environment \label{sec:tool-java}\<close> |
|
47825 | 56 |
|
61575 | 57 |
text \<open> |
58 |
The @{tool_def java} tool is a direct wrapper for the Java Runtime |
|
59 |
Environment, within the regular Isabelle settings environment |
|
71907 | 60 |
(\secref{sec:settings}) and Isabelle classpath. The command line arguments |
61 |
are that of the bundled Java distribution: see option \<^verbatim>\<open>-help\<close> in |
|
62 |
particular. |
|
47825 | 63 |
|
71907 | 64 |
The \<^verbatim>\<open>java\<close> executable is taken from @{setting ISABELLE_JDK_HOME}, according |
65 |
to the standard directory layout for regular distributions of OpenJDK. |
|
66 |
||
67 |
The shell function \<^bash_function>\<open>isabelle_jdk\<close> allows shell scripts to |
|
68 |
invoke other Java tools robustly (e.g.\ \<^verbatim>\<open>isabelle_jdk jar\<close>), without |
|
69 |
depending on accidental operating system installations. |
|
58618 | 70 |
\<close> |
47825 | 71 |
|
72 |
||
71907 | 73 |
subsection \<open>Scala toplevel \label{sec:tool-scala}\<close> |
47825 | 74 |
|
61575 | 75 |
text \<open> |
71907 | 76 |
The @{tool_def scala} tool is a direct wrapper for the Scala toplevel, |
77 |
similar to @{tool java} above. The command line arguments are that of the |
|
78 |
bundled Scala distribution: see option \<^verbatim>\<open>-help\<close> in particular. This allows |
|
79 |
to interact with Isabelle/Scala interactively. |
|
71897 | 80 |
\<close> |
81 |
||
82 |
subsubsection \<open>Example\<close> |
|
47825 | 83 |
|
71897 | 84 |
text \<open> |
85 |
Explore the Isabelle system environment in Scala: |
|
71907 | 86 |
@{verbatim [display, indent = 2] \<open>$ isabelle scala\<close>} |
87 |
@{scala [display, indent = 2] |
|
71897 | 88 |
\<open>import isabelle._ |
89 |
||
90 |
val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME") |
|
91 |
||
92 |
val options = Options.init() |
|
93 |
options.bool("browser_info") |
|
94 |
options.string("document")\<close>} |
|
58618 | 95 |
\<close> |
47825 | 96 |
|
97 |
||
71907 | 98 |
subsection \<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
|
99 |
|
61575 | 100 |
text \<open> |
101 |
The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"} |
|
102 |
allows to run Isabelle/Scala source files stand-alone programs, by using a |
|
62415 | 103 |
suitable ``hash-bang'' line and executable file permissions. For example: |
71907 | 104 |
@{verbatim [display, indent = 2] \<open>#!/usr/bin/env isabelle_scala_script\<close>} |
105 |
@{scala [display, indent = 2] |
|
106 |
\<open>val options = isabelle.Options.init() |
|
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
107 |
Console.println("browser_info = " + options.bool("browser_info")) |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
58618
diff
changeset
|
108 |
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
|
109 |
|
62415 | 110 |
This assumes that the executable may be found via the @{setting PATH} from |
111 |
the process environment: this is the case when Isabelle settings are active, |
|
112 |
e.g.\ in the context of the main Isabelle tool wrapper |
|
63680 | 113 |
\secref{sec:isabelle-tool}. Alternatively, the full |
114 |
\<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded |
|
62415 | 115 |
form. |
61575 | 116 |
\<close> |
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
117 |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
118 |
|
74041 | 119 |
subsection \<open>Scala compiler \label{sec:tool-scalac}\<close> |
120 |
||
121 |
text \<open> |
|
122 |
The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see |
|
123 |
also @{tool scala} above. The command line arguments are that of the |
|
124 |
bundled Scala distribution. |
|
125 |
||
126 |
This provides a low-level mechanism to compile further Scala modules, |
|
127 |
depending on existing Isabelle/Scala functionality; the resulting \<^verbatim>\<open>class\<close> |
|
128 |
or \<^verbatim>\<open>jar\<close> files can be added to the Java classpath using the shell function |
|
129 |
\<^bash_function>\<open>classpath\<close>. |
|
130 |
||
131 |
A more convenient high-level approach works via \<^path>\<open>etc/build.props\<close> |
|
132 |
(see \secref{sec:scala-build}). |
|
133 |
\<close> |
|
134 |
||
135 |
||
136 |
section \<open>Isabelle/Scala/Java modules \label{sec:scala-build}\<close> |
|
137 |
||
138 |
subsection \<open>Component configuration via \<^path>\<open>etc/build.props\<close>\<close> |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
139 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
140 |
text \<open> |
74041 | 141 |
Isabelle components may augment the Isabelle/Scala/Java environment |
142 |
declaratively via properties given in \<^path>\<open>etc/build.props\<close> (within the |
|
143 |
component directory). This specifies an output \<^verbatim>\<open>jar\<close> \<^emph>\<open>module\<close>, based on |
|
144 |
Scala or Java \<^emph>\<open>sources\<close>, and arbitrary \<^emph>\<open>resources\<close>. Moreover, a module can |
|
145 |
specify \<^emph>\<open>services\<close> that are subclasses of |
|
146 |
\<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>; these have a particular |
|
147 |
meaning to Isabelle/Scala tools. |
|
148 |
||
149 |
Before running a Scala or Java process, the Isabelle system implicitly |
|
150 |
ensures that all provided modules are compiled and packaged (as jars). It is |
|
151 |
also possible to invoke @{tool scala_build} explicitly, with extra options. |
|
152 |
||
153 |
\<^medskip> |
|
75161 | 154 |
The syntax of \<^path>\<open>etc/build.props\<close> follows a regular Java properties |
74041 | 155 |
file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/15/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>, |
156 |
but the encoding is \<^verbatim>\<open>UTF-8\<close>, instead of historic \<^verbatim>\<open>ISO 8859-1\<close> from the API |
|
157 |
documentation. |
|
158 |
||
159 |
The subsequent properties are relevant for the Scala/Java build process. |
|
160 |
Most properties are optional: the default is an empty string (or list). File |
|
161 |
names are relative to the main component directory and may refer to Isabelle |
|
162 |
settings variables (e.g. \<^verbatim>\<open>$ISABELLE_HOME\<close>). |
|
163 |
||
164 |
\<^item> \<^verbatim>\<open>title\<close> (required) is a human-readable description of the module, used |
|
165 |
in printed messages. |
|
166 |
||
167 |
\<^item> \<^verbatim>\<open>module\<close> specifies a \<^verbatim>\<open>jar\<close> file name for the output module, as result |
|
74057 | 168 |
of the specified sources (and resources). If this is absent (or |
169 |
\<^verbatim>\<open>no_build\<close> is set, as described below), there is no implicit build |
|
170 |
process. The contributing sources might be given nonetheless, notably for |
|
171 |
@{tool scala_project} (\secref{sec:tool-scala-project}), which includes |
|
172 |
Scala/Java sources of components, while suppressing \<^verbatim>\<open>jar\<close> modules (to |
|
173 |
avoid duplication of program content). |
|
74041 | 174 |
|
74057 | 175 |
\<^item> \<^verbatim>\<open>no_build\<close> is a Boolean property, with default \<^verbatim>\<open>false\<close>. If set to |
176 |
\<^verbatim>\<open>true\<close>, the implicit build process for the given \<^verbatim>\<open>module\<close> is \<^emph>\<open>omitted\<close> |
|
177 |
--- it is assumed to be provided by other means. |
|
74041 | 178 |
|
179 |
\<^item> \<^verbatim>\<open>scalac_options\<close> and \<^verbatim>\<open>javac_options\<close> augment the default settings |
|
180 |
@{setting_ref ISABELLE_SCALAC_OPTIONS} and @{setting_ref |
|
181 |
ISABELLE_JAVAC_OPTIONS} for this component; option syntax follows the |
|
182 |
regular command-line tools \<^verbatim>\<open>scalac\<close> and \<^verbatim>\<open>javac\<close>, respectively. |
|
183 |
||
184 |
\<^item> \<^verbatim>\<open>main\<close> specifies the main entry point for the \<^verbatim>\<open>jar\<close> module. This is |
|
185 |
only relevant for direct invocation like ``\<^verbatim>\<open>java -jar test.jar\<close>''. |
|
186 |
||
187 |
\<^item> \<^verbatim>\<open>requirements\<close> is a list of \<^verbatim>\<open>jar\<close> modules that are needed in the |
|
188 |
compilation process, but not provided by the regular classpath (notably |
|
189 |
@{setting ISABELLE_CLASSPATH}). |
|
190 |
||
74053 | 191 |
A \<^emph>\<open>normal entry\<close> refers to a single \<^verbatim>\<open>jar\<close> file name, possibly with |
74041 | 192 |
settings variables as usual. E.g. \<^file>\<open>$ISABELLE_SCALA_JAR\<close> for the main |
193 |
\<^file>\<open>$ISABELLE_HOME/lib/classes/isabelle.jar\<close> (especially relevant for |
|
194 |
add-on modules). |
|
195 |
||
75161 | 196 |
A \<^emph>\<open>special entry\<close> is of the form \<^verbatim>\<open>env:\<close>\<open>variable\<close> and refers to a |
74041 | 197 |
settings variable from the Isabelle environment: its value may consist of |
198 |
multiple \<^verbatim>\<open>jar\<close> entries (separated by colons). Environment variables are |
|
199 |
not expanded recursively. |
|
200 |
||
201 |
\<^item> \<^verbatim>\<open>resources\<close> is a list of files that should be included in the resulting |
|
202 |
\<^verbatim>\<open>jar\<close> file. Each item consists of a pair separated by colon: |
|
203 |
\<open>source\<close>\<^verbatim>\<open>:\<close>\<open>target\<close> means to copy an existing source file (relative to |
|
204 |
the component directory) to the given target file or directory (relative |
|
205 |
to the \<^verbatim>\<open>jar\<close> name space). A \<open>file\<close> specification without colon |
|
206 |
abbreviates \<open>file\<close>\<^verbatim>\<open>:\<close>\<open>file\<close>, i.e. the file is copied while retaining its |
|
207 |
relative path name. |
|
208 |
||
209 |
\<^item> \<^verbatim>\<open>sources\<close> is a list of \<^verbatim>\<open>.scala\<close> or \<^verbatim>\<open>.java\<close> files that contribute to |
|
210 |
the specified module. It is possible to use both languages simultaneously: |
|
211 |
the Scala and Java compiler will be invoked consecutively to make this |
|
212 |
work. |
|
213 |
||
214 |
\<^item> \<^verbatim>\<open>services\<close> is a list of class names to be registered as Isabelle |
|
215 |
service providers (subclasses of |
|
216 |
\<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>). Internal class names of |
|
217 |
the underlying JVM need to be given: e.g. see method @{scala_method (in |
|
218 |
java.lang.Object) getClass}. |
|
219 |
||
220 |
Particular services require particular subclasses: instances are filtered |
|
221 |
according to their dynamic type. For example, class |
|
222 |
\<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close> collects Scala command-line |
|
223 |
tools, and class \<^scala_type>\<open>isabelle.Scala.Functions\<close> collects Scala |
|
224 |
functions (\secref{sec:scala-functions}). |
|
225 |
\<close> |
|
226 |
||
227 |
||
228 |
subsection \<open>Explicit Isabelle/Scala/Java build \label{sec:tool-scala-build}\<close> |
|
229 |
||
230 |
text \<open> |
|
231 |
The @{tool_def scala_build} tool explicitly invokes the build process for |
|
232 |
all registered components. |
|
233 |
@{verbatim [display] |
|
234 |
\<open>Usage: isabelle scala_build [OPTIONS] |
|
235 |
||
236 |
Options are: |
|
237 |
-f force fresh build |
|
238 |
-q quiet mode: suppress stdout/stderr |
|
239 |
||
240 |
Build Isabelle/Scala/Java modules of all registered components |
|
241 |
(if required). |
|
242 |
\<close>} |
|
243 |
||
244 |
For each registered Isabelle component that provides |
|
245 |
\<^path>\<open>etc/build.props\<close>, the specified output \<^verbatim>\<open>module\<close> is checked against |
|
246 |
the corresponding input \<^verbatim>\<open>requirements\<close>, \<^verbatim>\<open>resources\<close>, \<^verbatim>\<open>sources\<close>. If |
|
247 |
required, there is an automatic build using \<^verbatim>\<open>scalac\<close> or \<^verbatim>\<open>javac\<close> (or both). |
|
248 |
The identity of input files is recorded within the output \<^verbatim>\<open>jar\<close>, using SHA1 |
|
249 |
digests in \<^verbatim>\<open>META-INF/isabelle/shasum\<close>. |
|
250 |
||
251 |
\<^medskip> |
|
252 |
Option \<^verbatim>\<open>-f\<close> forces a fresh build, regardless of the up-to-date status of |
|
253 |
input files vs. the output module. |
|
254 |
||
255 |
\<^medskip> |
|
256 |
Option \<^verbatim>\<open>-q\<close> suppresses all output on stdout/stderr produced by the Scala or |
|
257 |
Java compiler. |
|
258 |
||
259 |
\<^medskip> Explicit invocation of \<^verbatim>\<open>isabelle scala_build\<close> mainly serves testing or |
|
260 |
applications with special options: the Isabelle system normally does an |
|
261 |
automatic the build on demand. |
|
262 |
\<close> |
|
263 |
||
264 |
||
265 |
subsection \<open>Project setup for common Scala IDEs \label{sec:tool-scala-project}\<close> |
|
266 |
||
267 |
text \<open> |
|
268 |
The @{tool_def scala_project} tool creates a project configuration for all |
|
74960 | 269 |
Isabelle/Java/Scala modules specified in components via |
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
270 |
\<^path>\<open>etc/build.props\<close>, together with additional source files given on |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
271 |
the command-line: |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
272 |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
273 |
@{verbatim [display] |
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
274 |
\<open>Usage: isabelle scala_project [OPTIONS] [MORE_SOURCES ...] |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
275 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
276 |
Options are: |
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
277 |
-D DIR project directory (default: "$ISABELLE_HOME_USER/scala_project") |
74960 | 278 |
-G use Gradle as build tool |
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
279 |
-L make symlinks to original source files |
74960 | 280 |
-M use Maven as build tool |
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
281 |
-f force update of existing directory |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
282 |
|
74960 | 283 |
Setup project for Isabelle/Scala/jEdit --- to support common IDEs such |
284 |
as IntelliJ IDEA. Either option -G or -M is mandatory to specify the |
|
285 |
build tool.\<close>} |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
286 |
|
74960 | 287 |
The generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close> or |
288 |
Maven\<^footnote>\<open>\<^url>\<open>https://maven.apache.org\<close>\<close>, but the main purpose is to import it |
|
289 |
into common IDEs like IntelliJ IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. |
|
290 |
This allows to explore the sources with static analysis and other hints in |
|
291 |
real-time. |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
292 |
|
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
293 |
The generated files refer to physical file-system locations, using the path |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
294 |
notation of the underlying OS platform. Thus the project needs to be |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
295 |
recreated whenever the Isabelle installation is changed or moved. |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
296 |
|
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
297 |
\<^medskip> |
74960 | 298 |
Option \<^verbatim>\<open>-G\<close> selects Gradle and \<^verbatim>\<open>-M\<close> selects Maven as Java/Scala build |
299 |
tool: either one needs to be specified explicitly. These tools have a |
|
300 |
tendency to break down unexpectedly, so supporting both increases the |
|
301 |
chances that the generated IDE project works properly. |
|
302 |
||
303 |
\<^medskip> |
|
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
304 |
Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to |
74661
591303cc04c2
IDE build actually works (but somewhat pointless);
wenzelm
parents:
74656
diff
changeset
|
305 |
develop Isabelle/Scala/jEdit modules within an external IDE. The default is |
591303cc04c2
IDE build actually works (but somewhat pointless);
wenzelm
parents:
74656
diff
changeset
|
306 |
to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has no permanent |
591303cc04c2
IDE build actually works (but somewhat pointless);
wenzelm
parents:
74656
diff
changeset
|
307 |
effect on the originals. |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
308 |
|
71907 | 309 |
\<^medskip> |
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
310 |
Option \<^verbatim>\<open>-D\<close> specifies an explicit project directory, instead of the default |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
311 |
\<^path>\<open>$ISABELLE_HOME_USER/scala_project\<close>. Option \<^verbatim>\<open>-f\<close> forces an existing |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
312 |
project directory to be \<^emph>\<open>purged\<close> --- after some sanity checks that it has |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
313 |
been generated by @{tool "scala_project"} before. |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
314 |
\<close> |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
315 |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
316 |
|
74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
317 |
subsubsection \<open>Examples\<close> |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
318 |
|
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
319 |
text \<open> |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
320 |
Create a project directory and for editing the original sources: |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
321 |
|
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
322 |
@{verbatim [display] \<open>isabelle scala_project -f -L\<close>} |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
323 |
|
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
324 |
On Windows, this usually requires Administrator rights, in order to create |
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74057
diff
changeset
|
325 |
native symlinks. |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
326 |
\<close> |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
327 |
|
71907 | 328 |
|
329 |
section \<open>Registered Isabelle/Scala functions \label{sec:scala-functions}\<close> |
|
330 |
||
331 |
subsection \<open>Defining functions in Isabelle/Scala\<close> |
|
332 |
||
333 |
text \<open> |
|
74911
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
334 |
The service class \<^scala_type>\<open>isabelle.Scala.Functions\<close> collects Scala |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
335 |
functions of type \<^scala_type>\<open>isabelle.Scala.Fun\<close>: by registering |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
336 |
instances via \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close> |
75161 | 337 |
(\secref{sec:scala-build}), it becomes possible to invoke Isabelle/Scala |
74911
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
338 |
from Isabelle/ML (see below). |
71907 | 339 |
|
74911
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
340 |
An example is the predefined collection of |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
341 |
\<^scala_type>\<open>isabelle.Scala.Functions\<close> in |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
342 |
\<^file>\<open>$ISABELLE_HOME/etc/build.props\<close>. The overall list of registered functions |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
343 |
is accessible in Isabelle/Scala as |
71907 | 344 |
\<^scala_object>\<open>isabelle.Scala.functions\<close>. |
74911
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
345 |
|
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
346 |
The general class \<^scala_type>\<open>isabelle.Scala.Fun\<close> expects a multi-argument |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
347 |
/ multi-result function |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
348 |
\<^scala_type>\<open>List[isabelle.Bytes] => List[isabelle.Bytes]\<close>; more common are |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
349 |
instances of \<^scala_type>\<open>isabelle.Scala.Fun_Strings\<close> for type |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
350 |
\<^scala_type>\<open>List[String] => List[String]\<close>, or |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
351 |
\<^scala_type>\<open>isabelle.Scala.Fun_String\<close> for type |
74a800810bde
proper types for Scala.Fun instances (amending 1aa92bc4d356);
wenzelm
parents:
74661
diff
changeset
|
352 |
\<^scala_type>\<open>String => String\<close>. |
71907 | 353 |
\<close> |
354 |
||
355 |
||
356 |
subsection \<open>Invoking functions in Isabelle/ML\<close> |
|
357 |
||
358 |
text \<open> |
|
359 |
Isabelle/PIDE provides a protocol to invoke registered Scala functions in |
|
72103 | 360 |
ML: this works both within the Prover IDE and in batch builds. |
71907 | 361 |
|
362 |
The subsequent ML antiquotations refer to Scala functions in a |
|
363 |
formally-checked manner. |
|
364 |
||
365 |
\begin{matharray}{rcl} |
|
366 |
@{ML_antiquotation_def "scala_function"} & : & \<open>ML_antiquotation\<close> \\ |
|
367 |
@{ML_antiquotation_def "scala"} & : & \<open>ML_antiquotation\<close> \\ |
|
368 |
\end{matharray} |
|
369 |
||
370 |
\<^rail>\<open> |
|
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
371 |
(@{ML_antiquotation scala_function} | |
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
72759
diff
changeset
|
372 |
@{ML_antiquotation scala}) @{syntax embedded} |
71907 | 373 |
\<close> |
374 |
||
375 |
\<^descr> \<open>@{scala_function name}\<close> inlines the checked function name as ML string |
|
376 |
literal. |
|
377 |
||
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
378 |
\<^descr> \<open>@{scala name}\<close> and \<open>@{scala_thread name}\<close> invoke the checked function via |
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
379 |
the PIDE protocol. In Isabelle/ML this appears as a function of type |
74912 | 380 |
\<^ML_type>\<open>string list -> string list\<close> or \<^ML_type>\<open>string -> string\<close>, |
381 |
depending on the definition in Isabelle/Scala. Evaluation is subject to |
|
382 |
interrupts within the ML runtime environment as usual. A \<^scala>\<open>null\<close> |
|
383 |
result in Scala raises an exception \<^ML>\<open>Scala.Null\<close> in ML. The execution |
|
384 |
of \<open>@{scala}\<close> works via a Scala future on a bounded thread farm, while |
|
75161 | 385 |
\<open>@{scala_thread}\<close> always forks a separate Java/VM thread. |
71907 | 386 |
|
387 |
The standard approach of representing datatypes via strings works via XML in |
|
388 |
YXML transfer syntax. See Isabelle/ML operations and modules @{ML |
|
389 |
YXML.string_of_body}, @{ML YXML.parse_body}, @{ML_structure XML.Encode}, |
|
390 |
@{ML_structure XML.Decode}; similarly for Isabelle/Scala. Isabelle symbols |
|
391 |
may have to be recoded via Scala operations |
|
392 |
\<^scala_method>\<open>isabelle.Symbol.decode\<close> and |
|
393 |
\<^scala_method>\<open>isabelle.Symbol.encode\<close>. |
|
394 |
\<close> |
|
395 |
||
396 |
||
397 |
subsubsection \<open>Examples\<close> |
|
398 |
||
399 |
text \<open> |
|
72759 | 400 |
Invoke the predefined Scala function \<^scala_function>\<open>echo\<close>: |
71907 | 401 |
\<close> |
402 |
||
403 |
ML \<open> |
|
404 |
val s = "test"; |
|
405 |
val s' = \<^scala>\<open>echo\<close> s; |
|
406 |
\<^assert> (s = s') |
|
407 |
\<close> |
|
408 |
||
409 |
text \<open> |
|
410 |
Let the Scala compiler process some toplevel declarations, producing a list |
|
411 |
of errors: |
|
412 |
\<close> |
|
413 |
||
414 |
ML \<open> |
|
415 |
val source = "class A(a: Int, b: Boolean)" |
|
416 |
val errors = |
|
417 |
\<^scala>\<open>scala_toplevel\<close> source |
|
418 |
|> YXML.parse_body |
|
419 |
|> let open XML.Decode in list string end; |
|
420 |
||
421 |
\<^assert> (null errors)\<close> |
|
422 |
||
423 |
text \<open> |
|
424 |
The above is merely for demonstration. See \<^ML>\<open>Scala_Compiler.toplevel\<close> |
|
425 |
for a more convenient version with builtin decoding and treatment of errors. |
|
426 |
\<close> |
|
427 |
||
428 |
||
429 |
section \<open>Documenting Isabelle/Scala entities\<close> |
|
430 |
||
431 |
text \<open> |
|
432 |
The subsequent document antiquotations help to document Isabelle/Scala |
|
433 |
entities, with formal checking of names against the Isabelle classpath. |
|
434 |
||
435 |
\begin{matharray}{rcl} |
|
436 |
@{antiquotation_def "scala"} & : & \<open>antiquotation\<close> \\ |
|
437 |
@{antiquotation_def "scala_object"} & : & \<open>antiquotation\<close> \\ |
|
438 |
@{antiquotation_def "scala_type"} & : & \<open>antiquotation\<close> \\ |
|
439 |
@{antiquotation_def "scala_method"} & : & \<open>antiquotation\<close> \\ |
|
440 |
\end{matharray} |
|
441 |
||
442 |
\<^rail>\<open> |
|
443 |
(@@{antiquotation scala} | @@{antiquotation scala_object}) |
|
444 |
@{syntax embedded} |
|
445 |
; |
|
446 |
@@{antiquotation scala_type} @{syntax embedded} types |
|
447 |
; |
|
448 |
@@{antiquotation scala_method} class @{syntax embedded} types args |
|
449 |
; |
|
450 |
class: ('(' @'in' @{syntax name} types ')')? |
|
451 |
; |
|
452 |
types: ('[' (@{syntax name} ',' +) ']')? |
|
453 |
; |
|
454 |
args: ('(' (nat | (('_' | @{syntax name}) + ',')) ')')? |
|
455 |
\<close> |
|
456 |
||
457 |
\<^descr> \<open>@{scala s}\<close> is similar to \<open>@{verbatim s}\<close>, but the given source text is |
|
458 |
checked by the Scala compiler as toplevel declaration (without evaluation). |
|
459 |
This allows to write Isabelle/Scala examples that are statically checked. |
|
460 |
||
461 |
\<^descr> \<open>@{scala_object x}\<close> checks the given Scala object name (simple value or |
|
462 |
ground module) and prints the result verbatim. |
|
463 |
||
464 |
\<^descr> \<open>@{scala_type T[A]}\<close> checks the given Scala type name (with optional type |
|
465 |
parameters) and prints the result verbatim. |
|
466 |
||
467 |
\<^descr> \<open>@{scala_method (in c[A]) m[B](n)}\<close> checks the given Scala method \<open>m\<close> in |
|
468 |
the context of class \<open>c\<close>. The method argument slots are either specified by |
|
469 |
a number \<open>n\<close> or by a list of (optional) argument types; this may refer to |
|
470 |
type variables specified for the class or method: \<open>A\<close> or \<open>B\<close> above. |
|
471 |
||
472 |
Everything except for the method name \<open>m\<close> is optional. The absence of the |
|
473 |
class context means that this is a static method. The absence of arguments |
|
474 |
with types means that the method can be determined uniquely as \<^verbatim>\<open>(\<close>\<open>m\<close>\<^verbatim>\<open> _)\<close> |
|
475 |
in Scala (no overloading). |
|
476 |
\<close> |
|
477 |
||
478 |
||
479 |
subsubsection \<open>Examples\<close> |
|
480 |
||
481 |
text \<open> |
|
482 |
Miscellaneous Isabelle/Scala entities: |
|
483 |
||
484 |
\<^item> object: \<^scala_object>\<open>isabelle.Isabelle_Process\<close> |
|
485 |
\<^item> type without parameter: @{scala_type isabelle.Console_Progress} |
|
486 |
\<^item> type with parameter: @{scala_type List[A]} |
|
487 |
\<^item> static method: \<^scala_method>\<open>isabelle.Isabelle_System.bash\<close> |
|
488 |
\<^item> class and method with type parameters: |
|
489 |
@{scala_method (in List[A]) map[B]("A => B")} |
|
490 |
\<^item> overloaded method with argument type: @{scala_method (in Int) "+" (Int)} |
|
491 |
\<close> |
|
492 |
||
47825 | 493 |
end |