author | wenzelm |
Fri, 14 Aug 2020 13:26:12 +0200 | |
changeset 72151 | 64df1e514005 |
parent 72103 | 7b318273a4aa |
child 72156 | 065dcd80293e |
permissions | -rw-r--r-- |
71849 | 1 |
(* Title: Pure/System/scala.ML |
43748 | 2 |
Author: Makarius |
3 |
||
71849 | 4 |
Support for Scala at runtime. |
43748 | 5 |
*) |
6 |
||
71849 | 7 |
signature SCALA = |
43748 | 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 |
71881 | 11 |
val functions: unit -> string list |
12 |
val check_function: Proof.context -> string * Position.T -> string |
|
43748 | 13 |
end; |
14 |
||
71849 | 15 |
structure Scala: SCALA = |
43748 | 16 |
struct |
17 |
||
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
18 |
(** protocol for Scala function invocation from ML **) |
71849 | 19 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
20 |
exception Null; |
43749 | 21 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
22 |
local |
43748 | 23 |
|
52537 | 24 |
val new_id = string_of_int o Counter.make (); |
43748 | 25 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
26 |
val results = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
27 |
Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table); |
43748 | 28 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
29 |
val _ = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
30 |
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
|
31 |
(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
|
32 |
let |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
33 |
val result = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
34 |
(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
|
35 |
"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
|
36 |
| "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
|
37 |
| "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
|
38 |
| "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
|
39 |
| "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
|
40 |
| _ => 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
|
41 |
in Synchronized.change results (Symtab.map_entry id (K result)) end); |
43748 | 42 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
43 |
val _ = Session.protocol_handler "isabelle.Scala"; |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
44 |
|
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
45 |
in |
43748 | 46 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
47 |
fun function name arg = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
48 |
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
|
49 |
let |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
50 |
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
|
51 |
fun invoke () = |
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.update (id, Exn.Exn Match)); |
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.invoke_scala name id) [XML.Text arg]); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
54 |
fun cancel () = |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
55 |
(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
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
(fn tab => |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
60 |
(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
|
61 |
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
|
62 |
| 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
|
63 |
| 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
|
64 |
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
|
65 |
in |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
66 |
invoke (); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
67 |
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
|
68 |
end) (); |
43748 | 69 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
70 |
end; |
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
71 |
|
43748 | 72 |
|
73 |
||
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
74 |
(** registered Scala functions **) |
71872 | 75 |
|
71881 | 76 |
fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); |
71872 | 77 |
|
71911 | 78 |
fun check_function ctxt arg = |
71912 | 79 |
Completion.check_entity Markup.scala_functionN |
80 |
(functions () |> sort_strings |> map (rpair Position.none)) ctxt arg; |
|
71881 | 81 |
|
82 |
val _ = Theory.setup |
|
71898 | 83 |
(ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close> |
71881 | 84 |
(Args.context -- Scan.lift Parse.embedded_position |
85 |
>> (uncurry check_function #> ML_Syntax.print_string)) #> |
|
86 |
ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close> |
|
87 |
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => |
|
88 |
let val name = check_function ctxt arg |
|
89 |
in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end))); |
|
71872 | 90 |
|
43748 | 91 |
end; |