src/Tools/jEdit/src/jedit_resources.scala
changeset 59691 f6ff19188842
parent 59319 677615cba30d
child 60835 6512bb0b1ff4
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Mar 13 16:09:55 2015 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Mar 13 21:35:48 2015 +0100
     1.3 @@ -79,13 +79,6 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def check_file(view: View, file: String): Boolean =
     1.8 -    try {
     1.9 -      if (Url.is_wellformed(file)) Url.is_readable(file)
    1.10 -      else (new JFile(file)).isFile
    1.11 -    }
    1.12 -    catch { case ERROR(_) => false }
    1.13 -
    1.14  
    1.15    /* file content */
    1.16