author | Fabian Huch <huch@in.tum.de> |
Thu, 29 Sep 2022 13:58:26 +0200 | |
changeset 76222 | 3c4e373922ca |
parent 75577 | c51e1cef1eae |
child 78675 | f0a4ad78c0f2 |
permissions | -rw-r--r-- |
71849 | 1 |
(* Title: Pure/System/scala.ML |
43748 | 2 |
Author: Makarius |
3 |
||
73226
4c8edf348c4e
clarified modules: allow early invocation of Scala functions;
wenzelm
parents:
73225
diff
changeset
|
4 |
Invoke Scala functions from the ML 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 |
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
10 |
val function_bytes: string -> Bytes.T list -> Bytes.T list |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
11 |
val function1_bytes: string -> Bytes.T -> Bytes.T |
73565 | 12 |
val function: string -> string list -> string list |
13 |
val function1: string -> string -> string |
|
43748 | 14 |
end; |
15 |
||
71849 | 16 |
structure Scala: SCALA = |
43748 | 17 |
struct |
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 |
exception Null; |
43749 | 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 |
local |
43748 | 22 |
|
52537 | 23 |
val new_id = string_of_int o Counter.make (); |
43748 | 24 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
25 |
val results = |
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
26 |
Synchronized.var "Scala.results" (Symtab.empty: Bytes.T list Exn.result Symtab.table); |
43748 | 27 |
|
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
28 |
val _ = |
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
29 |
Protocol_Command.define_bytes "Scala.result" |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
30 |
(fn id :: tag :: rest => |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
31 |
let |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
32 |
val result = |
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
33 |
(case (Bytes.content tag, rest) of |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
34 |
("0", []) => Exn.Exn Null |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
35 |
| ("1", _) => Exn.Res rest |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
36 |
| ("2", [msg]) => Exn.Exn (ERROR (Bytes.content msg)) |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
37 |
| ("3", [msg]) => Exn.Exn (Fail (Bytes.content msg)) |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
38 |
| ("4", []) => Exn.Exn Exn.Interrupt |
73565 | 39 |
| _ => raise Fail "Malformed Scala.result"); |
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
40 |
in Synchronized.change results (Symtab.map_entry (Bytes.content id) (K result)) end); |
43748 | 41 |
|
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
73245
diff
changeset
|
42 |
in |
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
73245
diff
changeset
|
43 |
|
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
44 |
fun function_bytes name args = |
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)); |
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
50 |
Output.protocol_message (Markup.invoke_scala name id) (map Bytes.contents_blob args)); |
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) |
73245
f69cbb59813e
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
wenzelm
parents:
73226
diff
changeset
|
60 |
| NONE => SOME (Exn.Exn Exn.Interrupt, tab))); |
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
61 |
in |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
62 |
invoke (); |
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
63 |
Exn.release (restore_attributes await_result ()) |
73245
f69cbb59813e
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
wenzelm
parents:
73226
diff
changeset
|
64 |
handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn) |
72151
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 | 66 |
|
75577
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
67 |
val function1_bytes = singleton o function_bytes; |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
68 |
|
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
69 |
fun function name = map Bytes.string #> function_bytes name #> map Bytes.content; |
c51e1cef1eae
more scalable byte messages, notably for Scala functions in ML;
wenzelm
parents:
73565
diff
changeset
|
70 |
|
73565 | 71 |
val function1 = singleton o function; |
72 |
||
72151
64df1e514005
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
wenzelm
parents:
72103
diff
changeset
|
73 |
end; |
71871
28def00726ca
more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents:
71849
diff
changeset
|
74 |
|
43748 | 75 |
end; |