src/Pure/System/invoke_scala.ML
author wenzelm
Mon Jul 11 22:55:47 2011 +0200 (2011-07-11)
changeset 43761 e72ba84ae58f
parent 43749 5ca34f21cb44
child 44298 b8f8488704e2
permissions -rw-r--r--
tuned signature -- corresponding to Scala version;
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
  exception Null
wenzelm@43749
    12
  val method: string -> string -> string
wenzelm@43749
    13
  val promise_method: string -> string -> string future
wenzelm@43748
    14
  val fulfill_method: string -> string -> string -> unit
wenzelm@43748
    15
end;
wenzelm@43748
    16
wenzelm@43748
    17
structure Invoke_Scala: INVOKE_SCALA =
wenzelm@43748
    18
struct
wenzelm@43748
    19
wenzelm@43749
    20
exception Null;
wenzelm@43749
    21
wenzelm@43749
    22
wenzelm@43748
    23
(* pending promises *)
wenzelm@43748
    24
wenzelm@43748
    25
val new_id = string_of_int o Synchronized.counter ();
wenzelm@43748
    26
wenzelm@43748
    27
val promises =
wenzelm@43748
    28
  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
wenzelm@43748
    29
wenzelm@43748
    30
wenzelm@43748
    31
(* method invocation *)
wenzelm@43748
    32
wenzelm@43749
    33
fun promise_method name arg =
wenzelm@43748
    34
  let
wenzelm@43748
    35
    val id = new_id ();
wenzelm@43748
    36
    val promise = Future.promise () : string future;
wenzelm@43748
    37
    val _ = Synchronized.change promises (Symtab.update (id, promise));
wenzelm@43748
    38
    val _ = Output.raw_message (Markup.invoke_scala name id) arg;
wenzelm@43748
    39
  in promise end;
wenzelm@43748
    40
wenzelm@43749
    41
fun method name arg = Future.join (promise_method name arg);
wenzelm@43749
    42
wenzelm@43748
    43
wenzelm@43748
    44
(* fulfill method *)
wenzelm@43748
    45
wenzelm@43748
    46
fun fulfill_method id tag res =
wenzelm@43748
    47
  let
wenzelm@43748
    48
    val result =
wenzelm@43748
    49
      (case tag of
wenzelm@43748
    50
        "0" => Exn.Exn Null
wenzelm@43761
    51
      | "1" => Exn.Res res
wenzelm@43748
    52
      | "2" => Exn.Exn (ERROR res)
wenzelm@43748
    53
      | "3" => Exn.Exn (Fail res)
wenzelm@43748
    54
      | _ => raise Fail "Bad tag");
wenzelm@43748
    55
    val promise =
wenzelm@43748
    56
      Synchronized.change_result promises
wenzelm@43748
    57
        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
wenzelm@43748
    58
    val _ = Future.fulfill_result promise result;
wenzelm@43748
    59
  in () end;
wenzelm@43748
    60
wenzelm@43748
    61
end;
wenzelm@43748
    62