--- a/src/Pure/PIDE/protocol.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/PIDE/protocol.ML Thu Sep 28 14:43:07 2023 +0200
@@ -164,8 +164,9 @@
val _ =
Protocol_Command.define "Document.dialog_result"
(fn [serial, result] =>
- Active.dialog_result (Value.parse_int serial) result
- handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
+ (case Exn.capture (fn () => Active.dialog_result (Value.parse_int serial) result) () of
+ Exn.Res () => ()
+ | Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn));
val _ =
Protocol_Command.define "ML_Heap.full_gc"