# HG changeset patch
# User wenzelm
# Date 1695147879 -7200
# Node ID f0a4ad78c0f288645ef4552c2933845b1e4a05df
# Parent  88f47c70187a3e46f1b0a159b99c77b899773fc0
tuned;

diff -r 88f47c70187a -r f0a4ad78c0f2 src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Tue Sep 19 19:48:54 2023 +0200
+++ b/src/Pure/System/scala.ML	Tue Sep 19 20:24:39 2023 +0200
@@ -35,7 +35,7 @@
           | ("1", _) => Exn.Res rest
           | ("2", [msg]) => Exn.Exn (ERROR (Bytes.content msg))
           | ("3", [msg]) => Exn.Exn (Fail (Bytes.content msg))
-          | ("4", []) => Exn.Exn Exn.Interrupt
+          | ("4", []) => Exn.interrupt_exn
           | _ => raise Fail "Malformed Scala.result");
       in Synchronized.change results (Symtab.map_entry (Bytes.content id) (K result)) end);
 
@@ -57,7 +57,7 @@
             (case Symtab.lookup tab id of
               SOME (Exn.Exn Match) => NONE
             | SOME result => SOME (result, Symtab.delete id tab)
-            | NONE => SOME (Exn.Exn Exn.Interrupt, tab)));
+            | NONE => SOME (Exn.interrupt_exn, tab)));
     in
       invoke ();
       Exn.release (restore_attributes await_result ())