--- a/src/Pure/PIDE/rendering.scala Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Pure/PIDE/rendering.scala Sun Jan 01 22:54:40 2023 +0100
@@ -348,7 +348,7 @@
if (text == "" || text.endsWith("/")) (path, "")
else (path.dir, path.file_name)
- val directory = new JFile(session.resources.append(snapshot.node_name.master_dir, dir))
+ val directory = new JFile(session.resources.append_path(snapshot.node_name.master_dir, dir))
val files = directory.listFiles
if (files == null) Nil
else {
@@ -616,7 +616,7 @@
}
def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
- if (Path.is_valid(name)) session.resources.append(node_name.master_dir, Path.explode(name))
+ if (Path.is_valid(name)) session.resources.append_path(node_name.master_dir, Path.explode(name))
else name
def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = {