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;