author | wenzelm |
Wed, 27 Mar 2013 16:38:25 +0100 | |
changeset 51553 | 63327f679cff |
parent 50682 | a0888c03a727 |
child 52111 | 1fd184eaa310 |
permissions | -rw-r--r-- |
43748 | 1 |
(* Title: Pure/System/invoke_scala.ML |
2 |
Author: Makarius |
|
3 |
||
49173
fa01a202399c
eliminated potentially confusing terminology of Scala "layer";
wenzelm
parents:
46774
diff
changeset
|
4 |
JVM method invocation service via Isabelle/Scala. |
43748 | 5 |
*) |
6 |
||
7 |
signature INVOKE_SCALA = |
|
8 |
sig |
|
9 |
exception Null |
|
43749 | 10 |
val method: string -> string -> string |
11 |
val promise_method: string -> string -> string future |
|
43748 | 12 |
val fulfill_method: string -> string -> string -> unit |
13 |
end; |
|
14 |
||
15 |
structure Invoke_Scala: INVOKE_SCALA = |
|
16 |
struct |
|
17 |
||
43749 | 18 |
exception Null; |
19 |
||
20 |
||
43748 | 21 |
(* pending promises *) |
22 |
||
23 |
val new_id = string_of_int o Synchronized.counter (); |
|
24 |
||
25 |
val promises = |
|
26 |
Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table); |
|
27 |
||
28 |
||
29 |
(* method invocation *) |
|
30 |
||
43749 | 31 |
fun promise_method name arg = |
43748 | 32 |
let |
33 |
val id = new_id (); |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49470
diff
changeset
|
34 |
fun abort () = Output.protocol_message (Markup.cancel_scala id) ""; |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43761
diff
changeset
|
35 |
val promise = Future.promise abort : string future; |
43748 | 36 |
val _ = Synchronized.change promises (Symtab.update (id, promise)); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49470
diff
changeset
|
37 |
val _ = Output.protocol_message (Markup.invoke_scala name id) arg; |
43748 | 38 |
in promise end; |
39 |
||
43749 | 40 |
fun method name arg = Future.join (promise_method name arg); |
41 |
||
43748 | 42 |
|
43 |
(* fulfill method *) |
|
44 |
||
45 |
fun fulfill_method id tag res = |
|
46 |
let |
|
47 |
val result = |
|
48 |
(case tag of |
|
49 |
"0" => Exn.Exn Null |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43749
diff
changeset
|
50 |
| "1" => Exn.Res res |
43748 | 51 |
| "2" => Exn.Exn (ERROR res) |
52 |
| "3" => Exn.Exn (Fail res) |
|
49470 | 53 |
| "4" => Exn.Exn Exn.Interrupt |
43748 | 54 |
| _ => raise Fail "Bad tag"); |
55 |
val promise = |
|
56 |
Synchronized.change_result promises |
|
57 |
(fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); |
|
58 |
val _ = Future.fulfill_result promise result; |
|
59 |
in () end; |
|
60 |
||
61 |
end; |
|
62 |