src/Pure/PIDE/command.ML
changeset 78705 fde0b195cb7d
parent 78681 38fe769658be
child 78713 a44ac17ae227
--- a/src/Pure/PIDE/command.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -81,7 +81,7 @@
                   let val _ = Position.report pos (Markup.language_path delimited) in
                     case content of
                       NONE =>
-                        Exn.interruptible_capture (fn () =>
+                        Exn.result (fn () =>
                           Resources.read_file_node file_node master_dir (src_path, pos)) ()
                     | SOME (digest, lines) => Exn.Res (blob_file src_path lines digest file_node)
                   end