Method refresh

classpath/java/io/RandomAccessFile.java:50–55

()

    throws FileNotFoundException;

  private void refresh() throws IOException {
    if (file.length() != length) {
      close();
      open();
    }
  }

  public long length() throws IOException {
    refresh();