diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Wed Nov 28 15:38:18 2018 +0100 +++ b/src/Pure/PIDE/rendering.scala Wed Nov 28 16:14:31 2018 +0100 @@ -306,7 +306,7 @@ val path = Path.explode(text) val (dir, base_name) = if (text == "" || text.endsWith("/")) (path, "") - else (path.dir, path.base_name) + else (path.dir, path.file_name) val directory = new JFile(session.resources.append(snapshot.node_name, dir)) val files = directory.listFiles