src/Pure/System/scala.ML
author wenzelm
Sat, 28 Nov 2020 16:25:29 +0100
changeset 72759 bd5ee3148132
parent 72756 72ac27ea12b2
child 73225 3ab0cedaccad
permissions -rw-r--r--
more antiquotations (reverting 4df341249348);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
     1
(*  Title:      Pure/System/scala.ML
43748
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
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
     4
Support for Scala at runtime.
43748
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
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
     7
signature SCALA =
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
     8
sig
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
     9
  exception Null
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    10
  val function: string -> string -> string
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    11
  val function_thread: string -> string -> string
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    12
  val functions: unit -> string list
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    13
  val check_function: Proof.context -> string * Position.T -> string
43748
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
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
    16
structure Scala: SCALA =
43748
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
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    19
(** protocol for Scala function invocation from ML **)
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
    20
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    21
exception Null;
43749
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    22
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    23
local
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    24
52537
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents: 52111
diff changeset
    25
val new_id = string_of_int o Counter.make ();
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    26
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    27
val results =
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    28
  Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table);
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    29
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    30
val _ =
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    31
  Isabelle_Process.protocol_command "Scala.result"
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    32
    (fn [id, tag, res] =>
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    33
      let
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    34
        val result =
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    35
          (case tag of
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    36
            "0" => Exn.Exn Null
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    37
          | "1" => Exn.Res res
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    38
          | "2" => Exn.Exn (ERROR res)
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    39
          | "3" => Exn.Exn (Fail res)
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    40
          | "4" => Exn.Exn Exn.Interrupt
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    41
          | _ => raise Fail ("Bad tag: " ^ tag));
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    42
      in Synchronized.change results (Symtab.map_entry id (K result)) end);
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    43
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    44
fun gen_function thread name arg =
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    45
  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    46
    let
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    47
      val id = new_id ();
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    48
      fun invoke () =
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    49
       (Synchronized.change results (Symtab.update (id, Exn.Exn Match));
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    50
        Output.protocol_message (Markup.invoke_scala name id thread) [XML.Text arg]);
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    51
      fun cancel () =
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    52
       (Synchronized.change results (Symtab.delete_safe id);
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    53
        Output.protocol_message (Markup.cancel_scala id) []);
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    54
      fun await_result () =
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    55
        Synchronized.guarded_access results
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    56
          (fn tab =>
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    57
            (case Symtab.lookup tab id of
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    58
              SOME (Exn.Exn Match) => NONE
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    59
            | SOME result => SOME (result, Symtab.delete id tab)
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    60
            | NONE => SOME (Exn.Exn Exn.Interrupt, tab)))
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    61
        handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn);
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    62
    in
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    63
      invoke ();
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    64
      Exn.release (restore_attributes await_result ())
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    65
    end) ();
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    66
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    67
in
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    68
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    69
val function = gen_function false;
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    70
val function_thread = gen_function true;
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    71
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    72
end;
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    73
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    74
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    75
72151
64df1e514005 clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents: 72103
diff changeset
    76
(** registered Scala functions **)
71872
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
    77
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    78
fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
71872
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
    79
71911
d25093536482 clarified signature;
wenzelm
parents: 71898
diff changeset
    80
fun check_function ctxt arg =
71912
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    81
  Completion.check_entity Markup.scala_functionN
72756
72ac27ea12b2 more positions;
wenzelm
parents: 72332
diff changeset
    82
    (functions () |> sort_strings |> map (fn a => (a, Resources.scala_function_pos a))) ctxt arg;
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    83
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    84
val _ = Theory.setup
72759
bd5ee3148132 more antiquotations (reverting 4df341249348);
wenzelm
parents: 72756
diff changeset
    85
 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
bd5ee3148132 more antiquotations (reverting 4df341249348);
wenzelm
parents: 72756
diff changeset
    86
   (Scan.lift Parse.embedded_position) check_function #>
bd5ee3148132 more antiquotations (reverting 4df341249348);
wenzelm
parents: 72756
diff changeset
    87
  ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    88
    (Args.context -- Scan.lift Parse.embedded_position
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    89
      >> (uncurry check_function #> ML_Syntax.print_string)) #>
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    90
  ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    91
    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    92
      let val name = check_function ctxt arg
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    93
      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #>
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    94
  ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    95
    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    96
      let val name = check_function ctxt arg
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
    97
      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
71872
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
    98
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    99
end;