author | wenzelm |
Sat, 23 May 2020 21:43:30 +0200 | |
changeset 71871 | 28def00726ca |
parent 71849 | 265bbad3d6af |
child 71872 | b5191ededb6c |
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 |
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
9 |
val promise_function: string -> string -> string future |
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
10 |
val function: string -> string -> string |
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
11 |
val function_yxml: string -> XML.body -> XML.body |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
12 |
exception Null |
43748 | 13 |
end; |
14 |
||
71849 | 15 |
structure Scala: SCALA = |
43748 | 16 |
struct |
17 |
||
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
18 |
(** invoke Scala functions from ML **) |
71849 | 19 |
|
20 |
val _ = Session.protocol_handler "isabelle.Scala"; |
|
43749 | 21 |
|
22 |
||
43748 | 23 |
(* pending promises *) |
24 |
||
52537 | 25 |
val new_id = string_of_int o Counter.make (); |
43748 | 26 |
|
27 |
val promises = |
|
71849 | 28 |
Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table); |
43748 | 29 |
|
30 |
||
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
31 |
(* invoke function *) |
43748 | 32 |
|
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
33 |
fun promise_function name arg = |
43748 | 34 |
let |
35 |
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
|
36 |
fun abort () = Output.protocol_message (Markup.cancel_scala id) []; |
66166 | 37 |
val promise = Future.promise_name "invoke_scala" abort : string future; |
43748 | 38 |
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
|
39 |
val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]; |
43748 | 40 |
in promise end; |
41 |
||
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
42 |
fun function name arg = Future.join (promise_function name arg); |
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
43 |
|
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
44 |
fun function_yxml name = YXML.string_of_body #> function name #> YXML.parse_body; |
43749 | 45 |
|
43748 | 46 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
47 |
(* fulfill *) |
43748 | 48 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
49 |
exception Null; |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
50 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
51 |
fun fulfill id tag res = |
43748 | 52 |
let |
53 |
val result = |
|
54 |
(case tag of |
|
55 |
"0" => Exn.Exn Null |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43749
diff
changeset
|
56 |
| "1" => Exn.Res res |
43748 | 57 |
| "2" => Exn.Exn (ERROR res) |
58 |
| "3" => Exn.Exn (Fail res) |
|
49470 | 59 |
| "4" => Exn.Exn Exn.Interrupt |
43748 | 60 |
| _ => raise Fail "Bad tag"); |
61 |
val promise = |
|
62 |
Synchronized.change_result promises |
|
63 |
(fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); |
|
64 |
val _ = Future.fulfill_result promise result; |
|
65 |
in () end; |
|
66 |
||
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
67 |
val _ = |
71849 | 68 |
Isabelle_Process.protocol_command "Scala.fulfill" |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
69 |
(fn [id, tag, res] => |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
50682
diff
changeset
|
70 |
fulfill id tag res |
62505 | 71 |
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
|
72 |
|
43748 | 73 |
end; |