clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
authorwenzelm
Tue, 16 Apr 2019 19:42:56 +0200
changeset 70167 b33f28c81ba9
parent 70166 538919322852
child 70168 e79bbf86a984
clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Apr 14 18:13:46 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 16 19:42:56 2019 +0200
@@ -157,22 +157,22 @@
         }
 
       case None =>
-        val is_file =
+        val is_dir =
           try {
             val vfs = VFSManager.getVFSForPath(name)
             val vfs_file = vfs._getFile((), name, view)
-            vfs_file != null && vfs_file.getType == VFSFile.FILE
+            vfs_file != null && vfs_file.getType == VFSFile.DIRECTORY
           }
           catch { case ERROR(_) => false }
 
-        if (is_file) {
+        if (is_dir) VFSBrowser.browseDirectory(view, name)
+        else {
           val args =
             if (line <= 0) Array(name)
             else if (column <= 0) Array(name, "+line:" + (line + 1))
             else Array(name, "+line:" + (line + 1) + "," + (column + 1))
           jEdit.openFiles(view, null, args)
         }
-        else VFSBrowser.browseDirectory(view, name)
     }
   }