author | wenzelm |
Mon, 22 Feb 2021 12:30:05 +0100 | |
changeset 73273 | 17c28251fff0 |
parent 73245 | f69cbb59813e |
child 73419 | 22f3f2117ed7 |
permissions | -rw-r--r-- |
71849 | 1 |
(* Title: Pure/System/scala.ML |
43748 | 2 |
Author: Makarius |
3 |
||
73226
4c8edf348c4e
clarified modules: allow early invocation of Scala functions;
wenzelm
parents:
73225
diff
changeset
|
4 |
Invoke Scala functions from the ML runtime. |
43748 | 5 |
*) |
6 |
||
71849 | 7 |
signature SCALA = |
43748 | 8 |
sig |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
9 |
exception Null |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
10 |
val function: string -> string -> string |
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
11 |
val function_thread: string -> string -> string |
43748 | 12 |
end; |
13 |
||
71849 | 14 |
structure Scala: SCALA = |
43748 | 15 |
struct |
16 |
||
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
17 |
exception Null; |
43749 | 18 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
19 |
local |
43748 | 20 |
|
52537 | 21 |
val new_id = string_of_int o Counter.make (); |
43748 | 22 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
23 |
val results = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
24 |
Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table); |
43748 | 25 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
26 |
val _ = |
73225
3ab0cedaccad
clarified modules: allow early definition of protocol commands;
wenzelm
parents:
72759
diff
changeset
|
27 |
Protocol_Command.define "Scala.result" |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
28 |
(fn [id, tag, res] => |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
29 |
let |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
30 |
val result = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
31 |
(case tag of |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
32 |
"0" => Exn.Exn Null |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
33 |
| "1" => Exn.Res res |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
34 |
| "2" => Exn.Exn (ERROR res) |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
35 |
| "3" => Exn.Exn (Fail res) |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
36 |
| "4" => Exn.Exn Exn.Interrupt |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
37 |
| _ => raise Fail ("Bad tag: " ^ tag)); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
38 |
in Synchronized.change results (Symtab.map_entry id (K result)) end); |
43748 | 39 |
|
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
40 |
fun gen_function thread name arg = |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
41 |
Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
42 |
let |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
43 |
val id = new_id (); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
44 |
fun invoke () = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
45 |
(Synchronized.change results (Symtab.update (id, Exn.Exn Match)); |
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
46 |
Output.protocol_message (Markup.invoke_scala name id thread) [XML.Text arg]); |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
47 |
fun cancel () = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
48 |
(Synchronized.change results (Symtab.delete_safe id); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
49 |
Output.protocol_message (Markup.cancel_scala id) []); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
50 |
fun await_result () = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
51 |
Synchronized.guarded_access results |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
52 |
(fn tab => |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
53 |
(case Symtab.lookup tab id of |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
54 |
SOME (Exn.Exn Match) => NONE |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
55 |
| SOME result => SOME (result, Symtab.delete id tab) |
73245
f69cbb59813e
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
wenzelm
parents:
73226
diff
changeset
|
56 |
| NONE => SOME (Exn.Exn Exn.Interrupt, tab))); |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
57 |
in |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
58 |
invoke (); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
59 |
Exn.release (restore_attributes await_result ()) |
73245
f69cbb59813e
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
wenzelm
parents:
73226
diff
changeset
|
60 |
handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn) |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
61 |
end) (); |
43748 | 62 |
|
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
63 |
in |
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
64 |
|
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
65 |
val function = gen_function false; |
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
66 |
val function_thread = gen_function true; |
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
67 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
68 |
end; |
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
69 |
|
43748 | 70 |
end; |