src/Pure/System/invoke_scala.ML
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52537 4b5941730bd8
child 56333 38f1422ef473
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm@43748
     1
(*  Title:      Pure/System/invoke_scala.ML
wenzelm@43748
     2
    Author:     Makarius
wenzelm@43748
     3
wenzelm@49173
     4
JVM method invocation service via Isabelle/Scala.
wenzelm@43748
     5
*)
wenzelm@43748
     6
wenzelm@43748
     7
signature INVOKE_SCALA =
wenzelm@43748
     8
sig
wenzelm@43749
     9
  val method: string -> string -> string
wenzelm@43749
    10
  val promise_method: string -> string -> string future
wenzelm@52111
    11
  exception Null
wenzelm@43748
    12
end;
wenzelm@43748
    13
wenzelm@43748
    14
structure Invoke_Scala: INVOKE_SCALA =
wenzelm@43748
    15
struct
wenzelm@43748
    16
wenzelm@52111
    17
val _ = Session.protocol_handler "isabelle.Invoke_Scala";
wenzelm@43749
    18
wenzelm@43749
    19
wenzelm@43748
    20
(* pending promises *)
wenzelm@43748
    21
wenzelm@52537
    22
val new_id = string_of_int o Counter.make ();
wenzelm@43748
    23
wenzelm@43748
    24
val promises =
wenzelm@43748
    25
  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
wenzelm@43748
    26
wenzelm@43748
    27
wenzelm@43748
    28
(* method invocation *)
wenzelm@43748
    29
wenzelm@43749
    30
fun promise_method name arg =
wenzelm@43748
    31
  let
wenzelm@43748
    32
    val id = new_id ();
wenzelm@50201
    33
    fun abort () = Output.protocol_message (Markup.cancel_scala id) "";
wenzelm@44298
    34
    val promise = Future.promise abort : string future;
wenzelm@43748
    35
    val _ = Synchronized.change promises (Symtab.update (id, promise));
wenzelm@50201
    36
    val _ = Output.protocol_message (Markup.invoke_scala name id) arg;
wenzelm@43748
    37
  in promise end;
wenzelm@43748
    38
wenzelm@43749
    39
fun method name arg = Future.join (promise_method name arg);
wenzelm@43749
    40
wenzelm@43748
    41
wenzelm@52111
    42
(* fulfill *)
wenzelm@43748
    43
wenzelm@52111
    44
exception Null;
wenzelm@52111
    45
wenzelm@52111
    46
fun fulfill 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@49470
    54
      | "4" => Exn.Exn Exn.Interrupt
wenzelm@43748
    55
      | _ => raise Fail "Bad tag");
wenzelm@43748
    56
    val promise =
wenzelm@43748
    57
      Synchronized.change_result promises
wenzelm@43748
    58
        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
wenzelm@43748
    59
    val _ = Future.fulfill_result promise result;
wenzelm@43748
    60
  in () end;
wenzelm@43748
    61
wenzelm@52111
    62
val _ =
wenzelm@52111
    63
  Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
wenzelm@52111
    64
    (fn [id, tag, res] =>
wenzelm@52111
    65
      fulfill id tag res
wenzelm@52111
    66
        handle exn => if Exn.is_interrupt exn then () else reraise exn);
wenzelm@52111
    67
wenzelm@43748
    68
end;
wenzelm@43748
    69