--- a/src/Pure/System/scala.ML Sun Apr 11 21:32:09 2021 +0200
+++ b/src/Pure/System/scala.ML Sun Apr 11 22:47:55 2021 +0200
@@ -44,7 +44,7 @@
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) [[XML.Text arg]]);
fun cancel () =
(Synchronized.change results (Symtab.delete_safe id);
Output.protocol_message (Markup.cancel_scala id) []);