diff -r a5ff9cf61551 -r f2a8ba0b8c96 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 30 20:26:28 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 30 20:38:29 2022 +0100
@@ -114,6 +114,8 @@
           case _ => false
         }
 
+      def file_name: String = Url.get_base_name(node).getOrElse("")
+
       def path: Path = Path.explode(File.standard_path(node))
       def master_dir_path: Path = Path.explode(File.standard_path(master_dir))