src/Pure/System/invoke_scala.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 46774 38f113b052b1
child 49173 fa01a202399c
permissions -rw-r--r--
more official command specifications, including source position;
     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
    12   val method: string -> string -> string
    13   val promise_method: string -> string -> string future
    14   val fulfill_method: string -> string -> string -> unit
    15 end;
    16 
    17 structure Invoke_Scala: INVOKE_SCALA =
    18 struct
    19 
    20 exception Null;
    21 
    22 
    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 
    33 fun promise_method name arg =
    34   let
    35     val id = new_id ();
    36     fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) "";
    37     val promise = Future.promise abort : string future;
    38     val _ = Synchronized.change promises (Symtab.update (id, promise));
    39     val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg;
    40   in promise end;
    41 
    42 fun method name arg = Future.join (promise_method name arg);
    43 
    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
    52       | "1" => Exn.Res res
    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