# HG changeset patch
# User wenzelm
# Date 1661710907 -7200
# Node ID 63b22e3b80183687b07e1771e297496ba05eb83a
# Parent  9ac09016d03612da7e24f68edb85fd9eade9093a
tuned;

diff -r 9ac09016d036 -r 63b22e3b8018 src/Pure/PIDE/command.ML
--- 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;