src/Pure/System/invoke_scala.ML
author wenzelm
Wed May 22 14:10:45 2013 +0200 (2013-05-22 ago)
changeset 52111 1fd184eaa310
parent 50682 a0888c03a727
child 52537 4b5941730bd8
permissions -rw-r--r--
explicit management of Session.Protocol_Handlers, with protocol state and functions;
more self-contained ML/Scala module Invoke_Scala;
     1 (*  Title:      Pure/System/invoke_scala.ML
     2     Author:     Makarius
     3 
     4 JVM method invocation service via Isabelle/Scala.
     5 *)
     6 
     7 signature INVOKE_SCALA =
     8 sig
     9   val method: string -> string -> string
    10   val promise_method: string -> string -> string future
    11   exception Null
    12 end;
    13 
    14 structure Invoke_Scala: INVOKE_SCALA =
    15 struct
    16 
    17 val _ = Session.protocol_handler "isabelle.Invoke_Scala";
    18 
    19 
    20 (* pending promises *)
    21 
    22 val new_id = string_of_int o Synchronized.counter ();
    23 
    24 val promises =
    25   Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
    26 
    27 
    28 (* method invocation *)
    29 
    30 fun promise_method name arg =
    31   let
    32     val id = new_id ();
    33     fun abort () = Output.protocol_message (Markup.cancel_scala id) "";
    34     val promise = Future.promise abort : string future;
    35     val _ = Synchronized.change promises (Symtab.update (id, promise));
    36     val _ = Output.protocol_message (Markup.invoke_scala name id) arg;
    37   in promise end;
    38 
    39 fun method name arg = Future.join (promise_method name arg);
    40 
    41 
    42 (* fulfill *)
    43 
    44 exception Null;
    45 
    46 fun fulfill id tag res =
    47   let
    48     val result =
    49       (case tag of
    50         "0" => Exn.Exn Null
    51       | "1" => Exn.Res res
    52       | "2" => Exn.Exn (ERROR res)
    53       | "3" => Exn.Exn (Fail res)
    54       | "4" => Exn.Exn Exn.Interrupt
    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 val _ =
    63   Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
    64     (fn [id, tag, res] =>
    65       fulfill id tag res
    66         handle exn => if Exn.is_interrupt exn then () else reraise exn);
    67 
    68 end;
    69