src/Pure/System/invoke_scala.ML
changeset 52111 1fd184eaa310
parent 50682 a0888c03a727
child 52537 4b5941730bd8
     1.1 --- a/src/Pure/System/invoke_scala.ML	Wed May 22 08:46:39 2013 +0200
     1.2 +++ b/src/Pure/System/invoke_scala.ML	Wed May 22 14:10:45 2013 +0200
     1.3 @@ -6,16 +6,15 @@
     1.4  
     1.5  signature INVOKE_SCALA =
     1.6  sig
     1.7 -  exception Null
     1.8    val method: string -> string -> string
     1.9    val promise_method: string -> string -> string future
    1.10 -  val fulfill_method: string -> string -> string -> unit
    1.11 +  exception Null
    1.12  end;
    1.13  
    1.14  structure Invoke_Scala: INVOKE_SCALA =
    1.15  struct
    1.16  
    1.17 -exception Null;
    1.18 +val _ = Session.protocol_handler "isabelle.Invoke_Scala";
    1.19  
    1.20  
    1.21  (* pending promises *)
    1.22 @@ -40,9 +39,11 @@
    1.23  fun method name arg = Future.join (promise_method name arg);
    1.24  
    1.25  
    1.26 -(* fulfill method *)
    1.27 +(* fulfill *)
    1.28  
    1.29 -fun fulfill_method id tag res =
    1.30 +exception Null;
    1.31 +
    1.32 +fun fulfill id tag res =
    1.33    let
    1.34      val result =
    1.35        (case tag of
    1.36 @@ -58,5 +59,11 @@
    1.37      val _ = Future.fulfill_result promise result;
    1.38    in () end;
    1.39  
    1.40 +val _ =
    1.41 +  Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
    1.42 +    (fn [id, tag, res] =>
    1.43 +      fulfill id tag res
    1.44 +        handle exn => if Exn.is_interrupt exn then () else reraise exn);
    1.45 +
    1.46  end;
    1.47