diff -r a021bb558feb -r 1aa92bc4d356 src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML Mon Apr 12 15:00:03 2021 +0200 +++ b/src/Pure/System/scala.ML Mon Apr 12 18:10:13 2021 +0200 @@ -7,7 +7,8 @@ signature SCALA = sig exception Null - val function: string -> string -> string + val function: string -> string list -> string list + val function1: string -> string -> string end; structure Scala: SCALA = @@ -20,31 +21,31 @@ val new_id = string_of_int o Counter.make (); val results = - Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table); + Synchronized.var "Scala.results" (Symtab.empty: string list Exn.result Symtab.table); val _ = Protocol_Command.define "Scala.result" - (fn [id, tag, res] => + (fn id :: args => let val result = - (case tag of - "0" => Exn.Exn Null - | "1" => Exn.Res res - | "2" => Exn.Exn (ERROR res) - | "3" => Exn.Exn (Fail res) - | "4" => Exn.Exn Exn.Interrupt - | _ => raise Fail ("Bad tag: " ^ tag)); + (case args of + ["0"] => Exn.Exn Null + | "1" :: rest => Exn.Res rest + | ["2", msg] => Exn.Exn (ERROR msg) + | ["3", msg] => Exn.Exn (Fail msg) + | ["4"] => Exn.Exn Exn.Interrupt + | _ => raise Fail "Malformed Scala.result"); in Synchronized.change results (Symtab.map_entry id (K result)) end); in -fun function name arg = +fun function name args = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let val id = new_id (); fun invoke () = (Synchronized.change results (Symtab.update (id, Exn.Exn Match)); - Output.protocol_message (Markup.invoke_scala name id) [[XML.Text arg]]); + Output.protocol_message (Markup.invoke_scala name id) (map (single o XML.Text) args)); fun cancel () = (Synchronized.change results (Symtab.delete_safe id); Output.protocol_message (Markup.cancel_scala id) []); @@ -61,6 +62,8 @@ handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn) end) (); +val function1 = singleton o function; + end; end;