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