tuned;
authorwenzelm
Sun, 28 Aug 2022 20:21:47 +0200
changeset 76014 63b22e3b8018
parent 76013 9ac09016d036
child 76015 28445a0bd869
tuned;
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;