author | wenzelm |
Mon, 28 Nov 2011 22:05:32 +0100 | |
changeset 45666 | d83797ef0d2d |
parent 44298 | b8f8488704e2 |
child 46774 | 38f113b052b1 |
permissions | -rw-r--r-- |
43748 | 1 |
(* Title: Pure/System/invoke_scala.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
JVM method invocation service via Scala layer. |
|
5 |
||
6 |
TODO: proper cancellation! |
|
7 |
*) |
|
8 |
||
9 |
signature INVOKE_SCALA = |
|
10 |
sig |
|
11 |
exception Null |
|
43749 | 12 |
val method: string -> string -> string |
13 |
val promise_method: string -> string -> string future |
|
43748 | 14 |
val fulfill_method: string -> string -> string -> unit |
15 |
end; |
|
16 |
||
17 |
structure Invoke_Scala: INVOKE_SCALA = |
|
18 |
struct |
|
19 |
||
43749 | 20 |
exception Null; |
21 |
||
22 |
||
43748 | 23 |
(* pending promises *) |
24 |
||
25 |
val new_id = string_of_int o Synchronized.counter (); |
|
26 |
||
27 |
val promises = |
|
28 |
Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table); |
|
29 |
||
30 |
||
31 |
(* method invocation *) |
|
32 |
||
43749 | 33 |
fun promise_method name arg = |
43748 | 34 |
let |
35 |
val id = new_id (); |
|
45666 | 36 |
fun abort () = Output.raw_message (Isabelle_Markup.cancel_scala id) ""; |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43761
diff
changeset
|
37 |
val promise = Future.promise abort : string future; |
43748 | 38 |
val _ = Synchronized.change promises (Symtab.update (id, promise)); |
45666 | 39 |
val _ = Output.raw_message (Isabelle_Markup.invoke_scala name id) arg; |
43748 | 40 |
in promise end; |
41 |
||
43749 | 42 |
fun method name arg = Future.join (promise_method name arg); |
43 |
||
43748 | 44 |
|
45 |
(* fulfill method *) |
|
46 |
||
47 |
fun fulfill_method id tag res = |
|
48 |
let |
|
49 |
val result = |
|
50 |
(case tag of |
|
51 |
"0" => Exn.Exn Null |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43749
diff
changeset
|
52 |
| "1" => Exn.Res res |
43748 | 53 |
| "2" => Exn.Exn (ERROR res) |
54 |
| "3" => Exn.Exn (Fail res) |
|
55 |
| _ => raise Fail "Bad tag"); |
|
56 |
val promise = |
|
57 |
Synchronized.change_result promises |
|
58 |
(fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); |
|
59 |
val _ = Future.fulfill_result promise result; |
|
60 |
in () end; |
|
61 |
||
62 |
end; |
|
63 |