src/Pure/System/invoke_scala.ML
author wenzelm
Mon Jul 11 16:48:02 2011 +0200 (2011-07-11)
changeset 43748 c70bd78ec83c
child 43749 5ca34f21cb44
permissions -rw-r--r--
JVM method invocation service via Scala layer;
wenzelm@43748
     1
(*  Title:      Pure/System/invoke_scala.ML
wenzelm@43748
     2
    Author:     Makarius
wenzelm@43748
     3
wenzelm@43748
     4
JVM method invocation service via Scala layer.
wenzelm@43748
     5
wenzelm@43748
     6
TODO: proper cancellation!
wenzelm@43748
     7
*)
wenzelm@43748
     8
wenzelm@43748
     9
signature INVOKE_SCALA =
wenzelm@43748
    10
sig
wenzelm@43748
    11
  val method: string -> string -> string future
wenzelm@43748
    12
  exception Null
wenzelm@43748
    13
  val fulfill_method: string -> string -> string -> unit
wenzelm@43748
    14
end;
wenzelm@43748
    15
wenzelm@43748
    16
structure Invoke_Scala: INVOKE_SCALA =
wenzelm@43748
    17
struct
wenzelm@43748
    18
wenzelm@43748
    19
(* pending promises *)
wenzelm@43748
    20
wenzelm@43748
    21
val new_id = string_of_int o Synchronized.counter ();
wenzelm@43748
    22
wenzelm@43748
    23
val promises =
wenzelm@43748
    24
  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
wenzelm@43748
    25
wenzelm@43748
    26
wenzelm@43748
    27
(* method invocation *)
wenzelm@43748
    28
wenzelm@43748
    29
fun method name arg =
wenzelm@43748
    30
  let
wenzelm@43748
    31
    val id = new_id ();
wenzelm@43748
    32
    val promise = Future.promise () : string future;
wenzelm@43748
    33
    val _ = Synchronized.change promises (Symtab.update (id, promise));
wenzelm@43748
    34
    val _ = Output.raw_message (Markup.invoke_scala name id) arg;
wenzelm@43748
    35
  in promise end;
wenzelm@43748
    36
wenzelm@43748
    37
wenzelm@43748
    38
(* fulfill method *)
wenzelm@43748
    39
wenzelm@43748
    40
exception Null;
wenzelm@43748
    41
wenzelm@43748
    42
fun fulfill_method id tag res =
wenzelm@43748
    43
  let
wenzelm@43748
    44
    val result =
wenzelm@43748
    45
      (case tag of
wenzelm@43748
    46
        "0" => Exn.Exn Null
wenzelm@43748
    47
      | "1" => Exn.Result res
wenzelm@43748
    48
      | "2" => Exn.Exn (ERROR res)
wenzelm@43748
    49
      | "3" => Exn.Exn (Fail res)
wenzelm@43748
    50
      | _ => raise Fail "Bad tag");
wenzelm@43748
    51
    val promise =
wenzelm@43748
    52
      Synchronized.change_result promises
wenzelm@43748
    53
        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
wenzelm@43748
    54
    val _ = Future.fulfill_result promise result;
wenzelm@43748
    55
  in () end;
wenzelm@43748
    56
wenzelm@43748
    57
end;
wenzelm@43748
    58