src/Pure/System/scala.ML
author wenzelm
Tue, 26 May 2020 19:59:13 +0200
changeset 71898 4df341249348
parent 71881 71de0a253842
child 71911 d25093536482
permissions -rw-r--r--
discontinued pointless document antiquotation;
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
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
     9
  val functions: unit -> string list
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    10
  val check_function: Proof.context -> string * Position.T -> string
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    11
  val promise_function: string -> string -> string future
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    12
  val function: string -> string -> string
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    13
  exception Null
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
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    19
(** invoke Scala functions from ML **)
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
    20
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
    21
val _ = Session.protocol_handler "isabelle.Scala";
43749
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    22
5ca34f21cb44 tuned signature;
wenzelm
parents: 43748
diff changeset
    23
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    24
(* pending promises *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    25
52537
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents: 52111
diff changeset
    26
val new_id = string_of_int o Counter.make ();
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    27
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    28
val promises =
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
    29
  Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
43748
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
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    32
(* invoke function *)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    33
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    34
fun promise_function name arg =
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    35
  let
71876
ad063ac1f617 more robust: explicit check for PIDE session;
wenzelm
parents: 71873
diff changeset
    36
    val _ = if Resources.is_pide () then () else raise Fail "PIDE session required";
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    37
    val id = new_id ();
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 52537
diff changeset
    38
    fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
66166
c88d1c36c9c3 more informative task_statistics;
wenzelm
parents: 62505
diff changeset
    39
    val promise = Future.promise_name "invoke_scala" abort : string future;
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    40
    val _ = Synchronized.change promises (Symtab.update (id, promise));
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 66166
diff changeset
    41
    val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    42
  in promise end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    43
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    44
fun function name arg = Future.join (promise_function name arg);
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71849
diff changeset
    45
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    46
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    47
(* fulfill *)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    48
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    49
exception Null;
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    50
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    51
fun fulfill id tag res =
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    52
  let
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    53
    val result =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    54
      (case tag of
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    55
        "0" => Exn.Exn Null
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43749
diff changeset
    56
      | "1" => Exn.Res res
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    57
      | "2" => Exn.Exn (ERROR res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    58
      | "3" => Exn.Exn (Fail res)
49470
ee564db2649b more management of Invoke_Scala tasks;
wenzelm
parents: 49173
diff changeset
    59
      | "4" => Exn.Exn Exn.Interrupt
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    60
      | _ => raise Fail "Bad tag");
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    61
    val promise =
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    62
      Synchronized.change_result promises
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    63
        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    64
    val _ = Future.fulfill_result promise result;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    65
  in () end;
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
    66
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    67
val _ =
71849
265bbad3d6af clarified modules;
wenzelm
parents: 70991
diff changeset
    68
  Isabelle_Process.protocol_command "Scala.fulfill"
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    69
    (fn [id, tag, res] =>
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    70
      fulfill id tag res
62505
9e2a65912111 clarified modules;
wenzelm
parents: 56333
diff changeset
    71
        handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 50682
diff changeset
    72
71872
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
    73
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    74
(* registered functions *)
71872
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
    75
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    76
fun functions () = space_explode "," (getenv "ISABELLE_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 check_function ctxt (name, pos) =
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    79
  let
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    80
    val kind = Markup.scala_functionN;
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    81
    val funs = functions ();
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    82
  in
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    83
    if member (op =) funs name then
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    84
      (Context_Position.report ctxt pos (Markup.scala_function name); name)
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    85
    else
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    86
      let
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    87
        val completion_report =
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    88
          Completion.make_report (name, pos)
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    89
            (fn completed =>
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    90
              filter completed funs
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    91
              |> sort_strings
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    92
              |> map (fn a => (a, (kind, a))));
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    93
      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    94
  end;
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    95
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    96
val _ = Theory.setup
71898
4df341249348 discontinued pointless document antiquotation;
wenzelm
parents: 71881
diff changeset
    97
 (ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    98
    (Args.context -- Scan.lift Parse.embedded_position
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
    99
      >> (uncurry check_function #> ML_Syntax.print_string)) #>
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
   100
  ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
   101
    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
   102
      let val name = check_function ctxt arg
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 71876
diff changeset
   103
      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
71872
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
   104
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents:
diff changeset
   105
end;