author | wenzelm |
Sat, 13 Mar 2021 12:36:24 +0100 | |
changeset 73419 | 22f3f2117ed7 |
parent 72759 | bd5ee3148132 |
child 73987 | fc363a3b690a |
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 |
||
34 |
The main Isabelle/Scala functionality is provided by \<^verbatim>\<open>Pure.jar\<close>, but |
|
35 |
further add-ons are bundled with Isabelle, e.g.\ to access SQLite or |
|
36 |
PostgreSQL using JDBC (Java Database Connectivity). |
|
37 |
||
38 |
Other components may augment the system environment by providing a suitable |
|
39 |
\<^path>\<open>etc/settings\<close> shell script in the component directory. Some shell |
|
40 |
functions are available to help with that: |
|
41 |
||
42 |
\<^item> Function \<^bash_function>\<open>classpath\<close> adds \<^verbatim>\<open>jar\<close> files in Isabelle path |
|
43 |
notation (POSIX). On Windows, this is converted to native path names |
|
44 |
before invoking @{tool java} or @{tool scala} (\secref{sec:scala-tools}). |
|
45 |
||
46 |
\<^item> Function \<^bash_function>\<open>isabelle_scala_service\<close> registers global |
|
47 |
service providers as subclasses of |
|
48 |
\<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>, using the raw Java name |
|
49 |
according to @{scala_method (in java.lang.Object) getClass} (it should be |
|
50 |
enclosed in single quotes to avoid special characters like \<^verbatim>\<open>$\<close> to be |
|
51 |
interpreted by the shell). |
|
52 |
||
53 |
Particular Isabelle/Scala services require particular subclasses: |
|
54 |
instances are filtered according to their dynamic type. For example, class |
|
55 |
\<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close> collects Scala command-line |
|
72197 | 56 |
tools, and class \<^scala_type>\<open>isabelle.Scala.Functions\<close> |
71907 | 57 |
collects Scala functions (\secref{sec:scala-functions}). |
61575 | 58 |
\<close> |
47825 | 59 |
|
60 |
||
71907 | 61 |
section \<open>Command-line tools \label{sec:scala-tools}\<close> |
62 |
||
63 |
subsection \<open>Java Runtime Environment \label{sec:tool-java}\<close> |
|
47825 | 64 |
|
61575 | 65 |
text \<open> |
66 |
The @{tool_def java} tool is a direct wrapper for the Java Runtime |
|
67 |
Environment, within the regular Isabelle settings environment |
|
71907 | 68 |
(\secref{sec:settings}) and Isabelle classpath. The command line arguments |
69 |
are that of the bundled Java distribution: see option \<^verbatim>\<open>-help\<close> in |
|
70 |
particular. |
|
47825 | 71 |
|
71907 | 72 |
The \<^verbatim>\<open>java\<close> executable is taken from @{setting ISABELLE_JDK_HOME}, according |
73 |
to the standard directory layout for regular distributions of OpenJDK. |
|
74 |
||
75 |
The shell function \<^bash_function>\<open>isabelle_jdk\<close> allows shell scripts to |
|
76 |
invoke other Java tools robustly (e.g.\ \<^verbatim>\<open>isabelle_jdk jar\<close>), without |
|
77 |
depending on accidental operating system installations. |
|
58618 | 78 |
\<close> |
47825 | 79 |
|
80 |
||
71907 | 81 |
subsection \<open>Scala toplevel \label{sec:tool-scala}\<close> |
47825 | 82 |
|
61575 | 83 |
text \<open> |
71907 | 84 |
The @{tool_def scala} tool is a direct wrapper for the Scala toplevel, |
85 |
similar to @{tool java} above. The command line arguments are that of the |
|
86 |
bundled Scala distribution: see option \<^verbatim>\<open>-help\<close> in particular. This allows |
|
87 |
to interact with Isabelle/Scala interactively. |
|
71897 | 88 |
\<close> |
89 |
||
90 |
subsubsection \<open>Example\<close> |
|
47825 | 91 |
|
71897 | 92 |
text \<open> |
93 |
Explore the Isabelle system environment in Scala: |
|
71907 | 94 |
@{verbatim [display, indent = 2] \<open>$ isabelle scala\<close>} |
95 |
@{scala [display, indent = 2] |
|
71897 | 96 |
\<open>import isabelle._ |
97 |
||
98 |
val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME") |
|
99 |
||
100 |
val options = Options.init() |
|
101 |
options.bool("browser_info") |
|
102 |
options.string("document")\<close>} |
|
58618 | 103 |
\<close> |
47825 | 104 |
|
105 |
||
71907 | 106 |
subsection \<open>Scala compiler \label{sec:tool-scalac}\<close> |
47825 | 107 |
|
61575 | 108 |
text \<open> |
109 |
The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see |
|
110 |
also @{tool scala} above. The command line arguments are that of the |
|
71907 | 111 |
bundled Scala distribution. |
47825 | 112 |
|
113 |
This allows to compile further Scala modules, depending on existing |
|
71907 | 114 |
Isabelle/Scala functionality. The resulting \<^verbatim>\<open>class\<close> or \<^verbatim>\<open>jar\<close> files can be |
115 |
added to the Java classpath using the shell function |
|
116 |
\<^bash_function>\<open>classpath\<close>. Thus add-on components can register themselves |
|
117 |
in a modular manner, see also \secref{sec:components}. |
|
47825 | 118 |
|
71907 | 119 |
Note that Isabelle/jEdit @{cite "isabelle-jedit"} has its own mechanisms for |
120 |
adding plugin components. This needs special attention, since it overrides |
|
121 |
the standard Java class loader. |
|
61575 | 122 |
\<close> |
47825 | 123 |
|
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
124 |
|
71907 | 125 |
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
|
126 |
|
61575 | 127 |
text \<open> |
128 |
The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"} |
|
129 |
allows to run Isabelle/Scala source files stand-alone programs, by using a |
|
62415 | 130 |
suitable ``hash-bang'' line and executable file permissions. For example: |
71907 | 131 |
@{verbatim [display, indent = 2] \<open>#!/usr/bin/env isabelle_scala_script\<close>} |
132 |
@{scala [display, indent = 2] |
|
133 |
\<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
|
134 |
Console.println("browser_info = " + options.bool("browser_info")) |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
58618
diff
changeset
|
135 |
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
|
136 |
|
62415 | 137 |
This assumes that the executable may be found via the @{setting PATH} from |
138 |
the process environment: this is the case when Isabelle settings are active, |
|
139 |
e.g.\ in the context of the main Isabelle tool wrapper |
|
63680 | 140 |
\secref{sec:isabelle-tool}. Alternatively, the full |
141 |
\<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded |
|
62415 | 142 |
form. |
61575 | 143 |
\<close> |
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
144 |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
145 |
|
71907 | 146 |
subsection \<open>Project setup for common Scala IDEs\<close> |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
147 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
148 |
text \<open> |
71389 | 149 |
The @{tool_def scala_project} tool creates a project configuration for |
150 |
Isabelle/Scala/jEdit: |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
151 |
@{verbatim [display] |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
152 |
\<open>Usage: isabelle scala_project [OPTIONS] PROJECT_DIR |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
153 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
154 |
Options are: |
71503 | 155 |
-L make symlinks to original scala files |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
156 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
157 |
Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
158 |
such as IntelliJ IDEA.\<close>} |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
159 |
|
71389 | 160 |
The generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close>, but the |
161 |
main purpose is to import it into common Scala IDEs, such as IntelliJ |
|
162 |
IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore the |
|
163 |
sources with static analysis and other hints in real-time. |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
164 |
|
71907 | 165 |
The specified project directory needs to be fresh. The generated files refer |
166 |
to physical file-system locations, using the path notation of the underlying |
|
167 |
OS platform. Thus the project needs to be recreated whenever the Isabelle |
|
168 |
installation is changed or moved. |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
169 |
|
71907 | 170 |
\<^medskip> |
171 |
By default, Scala sources are \<^emph>\<open>copied\<close> from the Isabelle distribution and |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
172 |
editing them within the IDE has no permanent effect. |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
173 |
|
71523 | 174 |
Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to |
71389 | 175 |
develop Isabelle/Scala/jEdit within an external Scala IDE. Note that |
176 |
building the result always requires \<^verbatim>\<open>isabelle jedit -b\<close> on the |
|
177 |
command-line. |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
178 |
\<close> |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
179 |
|
71907 | 180 |
|
181 |
section \<open>Registered Isabelle/Scala functions \label{sec:scala-functions}\<close> |
|
182 |
||
183 |
subsection \<open>Defining functions in Isabelle/Scala\<close> |
|
184 |
||
185 |
text \<open> |
|
186 |
A Scala functions of type \<^scala_type>\<open>String => String\<close> may be wrapped as |
|
187 |
\<^scala_type>\<open>isabelle.Scala.Fun\<close> and collected via an instance of the |
|
72197 | 188 |
class \<^scala_type>\<open>isabelle.Scala.Functions\<close>. A system component |
71907 | 189 |
can then register that class via \<^bash_function>\<open>isabelle_scala_service\<close> |
190 |
in \<^path>\<open>etc/settings\<close> (\secref{sec:components}). An example is the |
|
72197 | 191 |
predefined collection of \<^scala_type>\<open>isabelle.Scala.Functions\<close> in |
71907 | 192 |
Isabelle/\<^verbatim>\<open>Pure.jar\<close> with the following line in |
193 |
\<^file>\<open>$ISABELLE_HOME/etc/settings\<close>: |
|
194 |
@{verbatim [display, indent = 2] \<open>isabelle_scala_service 'isabelle.Functions'\<close>} |
|
195 |
||
196 |
The overall list of registered functions is accessible in Isabelle/Scala as |
|
197 |
\<^scala_object>\<open>isabelle.Scala.functions\<close>. |
|
198 |
\<close> |
|
199 |
||
200 |
||
201 |
subsection \<open>Invoking functions in Isabelle/ML\<close> |
|
202 |
||
203 |
text \<open> |
|
204 |
Isabelle/PIDE provides a protocol to invoke registered Scala functions in |
|
72103 | 205 |
ML: this works both within the Prover IDE and in batch builds. |
71907 | 206 |
|
207 |
The subsequent ML antiquotations refer to Scala functions in a |
|
208 |
formally-checked manner. |
|
209 |
||
210 |
\begin{matharray}{rcl} |
|
211 |
@{ML_antiquotation_def "scala_function"} & : & \<open>ML_antiquotation\<close> \\ |
|
212 |
@{ML_antiquotation_def "scala"} & : & \<open>ML_antiquotation\<close> \\ |
|
213 |
\end{matharray} |
|
214 |
||
215 |
\<^rail>\<open> |
|
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
216 |
(@{ML_antiquotation scala_function} | |
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
72759
diff
changeset
|
217 |
@{ML_antiquotation scala}) @{syntax embedded} |
71907 | 218 |
\<close> |
219 |
||
220 |
\<^descr> \<open>@{scala_function name}\<close> inlines the checked function name as ML string |
|
221 |
literal. |
|
222 |
||
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
223 |
\<^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
|
224 |
the PIDE protocol. In Isabelle/ML this appears as a function of type |
71907 | 225 |
\<^ML_type>\<open>string -> string\<close>, which is subject to interrupts within the ML |
226 |
runtime environment as usual. A \<^scala>\<open>null\<close> result in Scala raises an |
|
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
227 |
exception \<^ML>\<open>Scala.Null\<close> in ML. The execution of \<open>@{scala}\<close> works via a |
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
228 |
Scala future on a bounded thread farm, while \<open>@{scala_thread}\<close> always forks |
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72252
diff
changeset
|
229 |
a separate Java thread. |
71907 | 230 |
|
231 |
The standard approach of representing datatypes via strings works via XML in |
|
232 |
YXML transfer syntax. See Isabelle/ML operations and modules @{ML |
|
233 |
YXML.string_of_body}, @{ML YXML.parse_body}, @{ML_structure XML.Encode}, |
|
234 |
@{ML_structure XML.Decode}; similarly for Isabelle/Scala. Isabelle symbols |
|
235 |
may have to be recoded via Scala operations |
|
236 |
\<^scala_method>\<open>isabelle.Symbol.decode\<close> and |
|
237 |
\<^scala_method>\<open>isabelle.Symbol.encode\<close>. |
|
238 |
\<close> |
|
239 |
||
240 |
||
241 |
subsubsection \<open>Examples\<close> |
|
242 |
||
243 |
text \<open> |
|
72759 | 244 |
Invoke the predefined Scala function \<^scala_function>\<open>echo\<close>: |
71907 | 245 |
\<close> |
246 |
||
247 |
ML \<open> |
|
248 |
val s = "test"; |
|
249 |
val s' = \<^scala>\<open>echo\<close> s; |
|
250 |
\<^assert> (s = s') |
|
251 |
\<close> |
|
252 |
||
253 |
text \<open> |
|
254 |
Let the Scala compiler process some toplevel declarations, producing a list |
|
255 |
of errors: |
|
256 |
\<close> |
|
257 |
||
258 |
ML \<open> |
|
259 |
val source = "class A(a: Int, b: Boolean)" |
|
260 |
val errors = |
|
261 |
\<^scala>\<open>scala_toplevel\<close> source |
|
262 |
|> YXML.parse_body |
|
263 |
|> let open XML.Decode in list string end; |
|
264 |
||
265 |
\<^assert> (null errors)\<close> |
|
266 |
||
267 |
text \<open> |
|
268 |
The above is merely for demonstration. See \<^ML>\<open>Scala_Compiler.toplevel\<close> |
|
269 |
for a more convenient version with builtin decoding and treatment of errors. |
|
270 |
\<close> |
|
271 |
||
272 |
||
273 |
section \<open>Documenting Isabelle/Scala entities\<close> |
|
274 |
||
275 |
text \<open> |
|
276 |
The subsequent document antiquotations help to document Isabelle/Scala |
|
277 |
entities, with formal checking of names against the Isabelle classpath. |
|
278 |
||
279 |
\begin{matharray}{rcl} |
|
280 |
@{antiquotation_def "scala"} & : & \<open>antiquotation\<close> \\ |
|
281 |
@{antiquotation_def "scala_object"} & : & \<open>antiquotation\<close> \\ |
|
282 |
@{antiquotation_def "scala_type"} & : & \<open>antiquotation\<close> \\ |
|
283 |
@{antiquotation_def "scala_method"} & : & \<open>antiquotation\<close> \\ |
|
284 |
\end{matharray} |
|
285 |
||
286 |
\<^rail>\<open> |
|
287 |
(@@{antiquotation scala} | @@{antiquotation scala_object}) |
|
288 |
@{syntax embedded} |
|
289 |
; |
|
290 |
@@{antiquotation scala_type} @{syntax embedded} types |
|
291 |
; |
|
292 |
@@{antiquotation scala_method} class @{syntax embedded} types args |
|
293 |
; |
|
294 |
class: ('(' @'in' @{syntax name} types ')')? |
|
295 |
; |
|
296 |
types: ('[' (@{syntax name} ',' +) ']')? |
|
297 |
; |
|
298 |
args: ('(' (nat | (('_' | @{syntax name}) + ',')) ')')? |
|
299 |
\<close> |
|
300 |
||
301 |
\<^descr> \<open>@{scala s}\<close> is similar to \<open>@{verbatim s}\<close>, but the given source text is |
|
302 |
checked by the Scala compiler as toplevel declaration (without evaluation). |
|
303 |
This allows to write Isabelle/Scala examples that are statically checked. |
|
304 |
||
305 |
\<^descr> \<open>@{scala_object x}\<close> checks the given Scala object name (simple value or |
|
306 |
ground module) and prints the result verbatim. |
|
307 |
||
308 |
\<^descr> \<open>@{scala_type T[A]}\<close> checks the given Scala type name (with optional type |
|
309 |
parameters) and prints the result verbatim. |
|
310 |
||
311 |
\<^descr> \<open>@{scala_method (in c[A]) m[B](n)}\<close> checks the given Scala method \<open>m\<close> in |
|
312 |
the context of class \<open>c\<close>. The method argument slots are either specified by |
|
313 |
a number \<open>n\<close> or by a list of (optional) argument types; this may refer to |
|
314 |
type variables specified for the class or method: \<open>A\<close> or \<open>B\<close> above. |
|
315 |
||
316 |
Everything except for the method name \<open>m\<close> is optional. The absence of the |
|
317 |
class context means that this is a static method. The absence of arguments |
|
318 |
with types means that the method can be determined uniquely as \<^verbatim>\<open>(\<close>\<open>m\<close>\<^verbatim>\<open> _)\<close> |
|
319 |
in Scala (no overloading). |
|
320 |
\<close> |
|
321 |
||
322 |
||
323 |
subsubsection \<open>Examples\<close> |
|
324 |
||
325 |
text \<open> |
|
326 |
Miscellaneous Isabelle/Scala entities: |
|
327 |
||
328 |
\<^item> object: \<^scala_object>\<open>isabelle.Isabelle_Process\<close> |
|
329 |
\<^item> type without parameter: @{scala_type isabelle.Console_Progress} |
|
330 |
\<^item> type with parameter: @{scala_type List[A]} |
|
331 |
\<^item> static method: \<^scala_method>\<open>isabelle.Isabelle_System.bash\<close> |
|
332 |
\<^item> class and method with type parameters: |
|
333 |
@{scala_method (in List[A]) map[B]("A => B")} |
|
334 |
\<^item> overloaded method with argument type: @{scala_method (in Int) "+" (Int)} |
|
335 |
\<close> |
|
336 |
||
47825 | 337 |
end |