Method fileFromURL

src/main/java/gate/util/Files.java:640–654

Convert a file: URL to a java.io.File . First tries to parse the URL's toExternalForm as a URI and create the File object from that URI. If this fails, just uses the path part of the URL. This handles URLs that contain spaces or other unusual characters, both as literals and when enco

(URL theURL)

   * File.
   */
  public static File fileFromURL(URL theURL) throws IllegalArgumentException {
    try {
      URI uri = new URI(theURL.toExternalForm());
      return new File(uri);
    }
    catch(URISyntaxException use) {
      try {
        URI uri = new URI(theURL.getProtocol(), null, theURL.getPath(), null, null);
        return new File(uri);
      }
      catch(URISyntaxException use2) {
        throw new IllegalArgumentException("Cannot convert " + theURL + " to a file path");
      }
    }
  }

  /**
   * Same as {@link java.io.File#listFiles(java.io.FileFilter)}