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