src/Pure/PIDE/resources.ML
changeset 72511 460d743010bc
parent 72162 5894859c5c84
child 72613 d01ea9e3bd2d
--- a/src/Pure/PIDE/resources.ML	Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Oct 27 22:34:37 2020 +0100
@@ -155,7 +155,7 @@
     val dirs = Symtab.lookup_list (get_session_base #session_directories) session;
   in
     dirs |> get_first (fn dir =>
-      let val path = Path.append dir thy_file
+      let val path = dir + thy_file
       in if File.is_file path then SOME path else NONE end)
   end;
 
@@ -257,7 +257,7 @@
       (case opt_dir of
         SOME dir => dir
       | NONE => master_directory (Proof_Context.theory_of ctxt));
-    val path = Path.append dir (Path.explode name) handle ERROR msg => err msg;
+    val path = dir + Path.explode name handle ERROR msg => err msg;
     val _ = Path.expand path handle ERROR msg => err msg;
     val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
     val _ = check_file path handle ERROR msg => err msg;