more robust;
authorwenzelm
Mon, 26 Dec 2022 19:00:00 +0100
changeset 76782 a62a609b5db2
parent 76781 d9f48960bf23
child 76783 8ebde8164bba
more robust;
src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 26 18:41:27 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 26 19:00:00 2022 +0100
@@ -59,10 +59,10 @@
   }
 
 
-  /* files */
+  /* plain files */
 
   def is_file(name: String): Boolean =
-    VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
+    name != null && name.nonEmpty && VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
 
   def check_file(name: String): Option[JFile] =
     if (is_file(name)) Some(new JFile(name)) else None