src/Pure/System/invoke_scala.ML
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 46774 38f113b052b1
child 49173 fa01a202399c
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/invoke_scala.ML
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     3
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     4
JVM method invocation service via Scala layer.
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     5
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     6
TODO: proper cancellation!
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     7
*)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     8
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     9
signature INVOKE_SCALA =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    10
sig
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    11
  exception Null
43749
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    12
  val method: string -> string -> string
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    13
  val promise_method: string -> string -> string future
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    14
  val fulfill_method: string -> string -> string -> unit
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    15
end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    16
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    17
structure Invoke_Scala: INVOKE_SCALA =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    18
struct
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    19
43749
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    20
exception Null;
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    21
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    22
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    23
(* pending promises *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    24
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    25
val new_id = string_of_int o Synchronized.counter ();
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    26
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    27
val promises =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    28
  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    29
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    30
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    31
(* method invocation *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    32
43749
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    33
fun promise_method name arg =
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    34
  let
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    35
    val id = new_id ();
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 45666
diff changeset
    36
    fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) "";
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43761
diff changeset
    37
    val promise = Future.promise abort : string future;
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    38
    val _ = Synchronized.change promises (Symtab.update (id, promise));
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 45666
diff changeset
    39
    val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg;
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    40
  in promise end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    41
43749
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    42
fun method name arg = Future.join (promise_method name arg);
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    43
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    44
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    45
(* fulfill method *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    46
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    47
fun fulfill_method id tag res =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    48
  let
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    49
    val result =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    50
      (case tag of
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    51
        "0" => Exn.Exn Null
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43749
diff changeset
    52
      | "1" => Exn.Res res
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    53
      | "2" => Exn.Exn (ERROR res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    54
      | "3" => Exn.Exn (Fail res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    55
      | _ => raise Fail "Bad tag");
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    56
    val promise =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    57
      Synchronized.change_result promises
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    58
        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    59
    val _ = Future.fulfill_result promise result;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    60
  in () end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    61
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    62
end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    63