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;
     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   val method: string -> string -> string future
    12   exception Null
    13   val fulfill_method: string -> string -> string -> unit
    14 end;
    15 
    16 structure Invoke_Scala: INVOKE_SCALA =
    17 struct
    18 
    19 (* pending promises *)
    20 
    21 val new_id = string_of_int o Synchronized.counter ();
    22 
    23 val promises =
    24   Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
    25 
    26 
    27 (* method invocation *)
    28 
    29 fun method name arg =
    30   let
    31     val id = new_id ();
    32     val promise = Future.promise () : string future;
    33     val _ = Synchronized.change promises (Symtab.update (id, promise));
    34     val _ = Output.raw_message (Markup.invoke_scala name id) arg;
    35   in promise end;
    36 
    37 
    38 (* fulfill method *)
    39 
    40 exception Null;
    41 
    42 fun fulfill_method id tag res =
    43   let
    44     val result =
    45       (case tag of
    46         "0" => Exn.Exn Null
    47       | "1" => Exn.Result res
    48       | "2" => Exn.Exn (ERROR res)
    49       | "3" => Exn.Exn (Fail res)
    50       | _ => raise Fail "Bad tag");
    51     val promise =
    52       Synchronized.change_result promises
    53         (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
    54     val _ = Future.fulfill_result promise result;
    55   in () end;
    56 
    57 end;
    58