@@ -0,0 +1,3246 @@
+package org.plumelib.util;%0A%0Aimport java.io.File;%0Aimport java.io.FileWriter;%0Aimport java.io.IOException;%0Aimport org.checkerframework.checker.lock.qual.GuardedByUnknown;%0Aimport org.checkerframework.dataflow.qual.Pure;%0A%0A/** Just like FileWriter, but adds a getFileName() method and overrides toString(). */%0Apublic final class FileWriterWithName extends FileWriter %7B%0A%0A  private final String fileName;%0A%0A  /**%0A   * Constructs a FileWriterWithName object given a file name.%0A   *%0A   * @param fileName String The system-dependent filename.%0A   * @throws IOException if the named file exists but is a directory rather than a regular file,%0A   *     does not exist but cannot be created, or cannot be opened for any other reason%0A   */%0A  public FileWriterWithName(String fileName) throws IOException %7B%0A    super(fileName);%0A    this.fileName = fileName;%0A  %7D%0A%0A  /**%0A   * Constructs a FileWriterWithName object given a file name with a boolean indicating whether or%0A   * not to append the data written.%0A   *%0A   * @param fileName String The system-dependent filename.%0A   * @param append boolean if %7B@code true%7D, then data will be written to the end of the file rather%0A   *     than the beginning.%0A   * @throws IOException if the named file exists but is a directory rather than a regular file,%0A   *     does not exist but cannot be created, or cannot be opened for any other reason%0A   */%0A  public FileWriterWithName(String fileName, boolean append) throws IOException %7B%0A    super(fileName, append);%0A    this.fileName = fileName;%0A  %7D%0A%0A  /**%0A   * Constructs a FileWriterWithName object given a File object.%0A   *%0A   * @param file a File object to write to.%0A   * @throws IOException if the file exists but is a directory rather than a regular file, does not%0A   *     exist but cannot be created, or cannot be opened for any other reason%0A   */%0A  public FileWriterWithName(File file) throws IOException %7B%0A    super(file);%0A    this.fileName = file.getAbsolutePath();%0A  %7D%0A%0A  /**%0A   * Constructs a FileWriterWithName object given a File object. If the second argument is %7B@code%0A   * true%7D, then bytes will be written to the end of the file rather than the beginning.%0A   *%0A   * @param file a File object to write to%0A   * @param append if %7B@code true%7D, then bytes will be written to the end of the file rather than%0A   *     the beginning%0A   * @throws IOException if the file exists but is a directory rather than a regular file, does not%0A   *     exist but cannot be created, or cannot be opened for any other reason%0A   * @since 1.4%0A   */%0A  public FileWriterWithName(File file, boolean append) throws IOException %7B%0A    super(file, append);%0A    this.fileName = file.getAbsolutePath();%0A  %7D%0A%0A  /**%0A   * Return the name of the file being written by this.%0A   *%0A   * @return the name of the file being written by this%0A   */%0A  @SuppressWarnings(%22lock%22) // Lock Checker bug? fileName is final, no lock is needed to access it%0A  @Pure%0A  public String getFileName(@GuardedByUnknown FileWriterWithName this) %7B%0A    return fileName;%0A  %7D%0A%0A  /**%0A   * Return the name of the file being written by this.%0A   *%0A   * @return the name of the file being written by this%0A   */%0A  @Pure%0A  @Override%0A  public String toString(@GuardedByUnknown FileWriterWithName this) %7B%0A    return getFileName();%0A  %7D%0A%7D%0A

Add FileWriterWithName class