author | wenzelm |
Wed, 20 May 2020 20:45:43 +0200 | |
changeset 71849 | 265bbad3d6af |
parent 70991 | src/Pure/System/invoke_scala.ML@f9f7c34b7dd4 |
child 71871 | 28def00726ca |
permissions | -rw-r--r-- |
71849 | 1 |
(* Title: Pure/System/scala.ML |
43748 | 2 |
Author: Makarius |
3 |
||
71849 | 4 |
Support for Scala at runtime. |
43748 | 5 |
*) |
6 |
||
71849 | 7 |
signature SCALA = |
43748 | 8 |
sig |
43749 | 9 |
val method: string -> string -> string |
10 |
val promise_method: string -> string -> string future |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
11 |
exception Null |
43748 | 12 |
end; |
13 |
||
71849 | 14 |
structure Scala: SCALA = |
43748 | 15 |
struct |
16 |
||
71849 | 17 |
(** invoke JVM method via Isabelle/Scala **) |
18 |
||
19 |
val _ = Session.protocol_handler "isabelle.Scala"; |
|
43749 | 20 |
|
21 |
||
43748 | 22 |
(* pending promises *) |
23 |
||
52537 | 24 |
val new_id = string_of_int o Counter.make (); |
43748 | 25 |
|
26 |
val promises = |
|
71849 | 27 |
Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table); |
43748 | 28 |
|
29 |
||
30 |
(* method invocation *) |
|
31 |
||
43749 | 32 |
fun promise_method name arg = |
43748 | 33 |
let |
34 |
val id = new_id (); |
|
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
52537
diff
changeset
|
35 |
fun abort () = Output.protocol_message (Markup.cancel_scala id) []; |
66166 | 36 |
val promise = Future.promise_name "invoke_scala" abort : string future; |
43748 | 37 |
val _ = Synchronized.change promises (Symtab.update (id, promise)); |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
66166
diff
changeset
|
38 |
val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]; |
43748 | 39 |
in promise end; |
40 |
||
43749 | 41 |
fun method name arg = Future.join (promise_method name arg); |
42 |
||
43748 | 43 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
44 |
(* fulfill *) |
43748 | 45 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
46 |
exception Null; |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
47 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
48 |
fun fulfill id tag res = |
43748 | 49 |
let |
50 |
val result = |
|
51 |
(case tag of |
|
52 |
"0" => Exn.Exn Null |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43749
diff
changeset
|
53 |
| "1" => Exn.Res res |
43748 | 54 |
| "2" => Exn.Exn (ERROR res) |
55 |
| "3" => Exn.Exn (Fail res) |
|
49470 | 56 |
| "4" => Exn.Exn Exn.Interrupt |
43748 | 57 |
| _ => raise Fail "Bad tag"); |
58 |
val promise = |
|
59 |
Synchronized.change_result promises |
|
60 |
(fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); |
|
61 |
val _ = Future.fulfill_result promise result; |
|
62 |
in () end; |
|
63 |
||
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
64 |
val _ = |
71849 | 65 |
Isabelle_Process.protocol_command "Scala.fulfill" |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
66 |
(fn [id, tag, res] => |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
67 |
fulfill id tag res |
62505 | 68 |
handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
69 |
|
43748 | 70 |
end; |