--- a/src/Pure/PIDE/command.ML Sun Aug 28 14:55:40 2022 +0200
+++ b/src/Pure/PIDE/command.ML Sun Aug 28 20:21:47 2022 +0200
@@ -63,14 +63,14 @@
if Context_Position.pide_reports ()
then Position.report pos (Markup.language_path delimited) else ();
- fun read_file () =
+ fun read_local () =
let
val path = File.check_file (File.full_path master_dir src_path);
val text = File.read path;
val file_pos = Path.position path;
in (text, file_pos) end;
- fun read_url () =
+ fun read_remote () =
let
val text = Bytes.content (Isabelle_System.download file_node);
val file_pos = Position.file file_node;
@@ -78,9 +78,9 @@
val (text, file_pos) =
(case try Url.explode file_node of
- NONE => read_file ()
- | SOME (Url.File _) => read_file ()
- | _ => read_url ());
+ NONE => read_local ()
+ | SOME (Url.File _) => read_local ()
+ | _ => read_remote ());
val lines = split_lines text;
val digest = SHA1.digest text;