src/Pure/System/scala.ML
changeset 73559 22b5ecb53dd9
parent 73419 22f3f2117ed7
child 73565 1aa92bc4d356
--- 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) []);