src/Pure/System/invoke_scala.ML
author wenzelm
Mon, 11 Jul 2011 16:48:02 +0200
changeset 43748 c70bd78ec83c
child 43749 5ca34f21cb44
permissions -rw-r--r--
JVM method invocation service via Scala layer;
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
  val method: string -> string -> string future
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    12
  exception Null
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    13
  val fulfill_method: string -> string -> string -> unit
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    14
end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    15
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    16
structure Invoke_Scala: INVOKE_SCALA =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    17
struct
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    18
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    19
(* pending promises *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    20
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    21
val new_id = string_of_int o Synchronized.counter ();
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    22
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    23
val promises =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    24
  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    25
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
(* method invocation *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    28
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    29
fun method name arg =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    30
  let
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    31
    val id = new_id ();
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    32
    val promise = Future.promise () : string future;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    33
    val _ = Synchronized.change promises (Symtab.update (id, promise));
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    34
    val _ = Output.raw_message (Markup.invoke_scala name id) arg;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    35
  in promise end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    36
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    37
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    38
(* fulfill method *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    39
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    40
exception Null;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    41
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    42
fun fulfill_method id tag res =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    43
  let
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    44
    val result =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    45
      (case tag of
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    46
        "0" => Exn.Exn Null
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    47
      | "1" => Exn.Result res
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    48
      | "2" => Exn.Exn (ERROR res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    49
      | "3" => Exn.Exn (Fail res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    50
      | _ => raise Fail "Bad tag");
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    51
    val promise =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    52
      Synchronized.change_result promises
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    53
        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    54
    val _ = Future.fulfill_result promise result;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    55
  in () end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    56
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    57
end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    58