content: /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
   *
   * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
   * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
   * merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
   * furnished to do so, subject to the following conditions:
   *
   * The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
   *
   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
   * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
   * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
   * OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
   */
  
  package edu.mit.csail.sdg.alloy4;
  
  import java.awt.Color;
  import java.awt.Polygon;
  import java.awt.Shape;
  import java.awt.geom.PathIterator;
  import java.io.IOException;
  import java.io.RandomAccessFile;
  
  /**
   * Graphical convenience methods for producing PDF files.
   * <p>
   * This implementation explicitly generates a very simple 8.5 inch by 11 inch
   * one-page PDF consisting of graphical operations. Hopefully this class will no
   * longer be needed in the future once Java comes with better PDF support.
   */
  
  public final strictfp class OurPDFWriter {
  
      /** The filename. */
      private final String filename;
  
      /** The page width (in terms of dots). */
      private final long   width;
  
      /** The page height (in terms of dots). */
      private final long   height;
  
      /**
       * Latest color expressed as RGB (-1 if none has been explicitly set so far)
       */
      private int          color = -1;
  
      /**
       * Latest line style (0=normal, 1=bold, 2=dotted, 3=dashed)
       */
      private int          line  = 0;
  
      /**
       * The buffer that will store the list of graphical operations issued so far
       * (null if close() has been called successfully)
       */
      private ByteBuffer   buf   = new ByteBuffer();
  
      /**
       * Begin a blank PDF file with the given dots-per-inch and the given scale (the
       * given file, if existed, will be overwritten)
       *
       * @throws IllegalArgumentException if dpi is less than 50 or is greater than
       *             3000
       */
      public OurPDFWriter(String filename, int dpi, double scale) {
          if (dpi < 50 || dpi > 3000)
              throw new IllegalArgumentException("The DPI must be between 50 and 3000");
          this.filename = filename;
          width = dpi * 8L + (dpi / 2L); // "8.5 inches"
          height = dpi * 11L; // "11 inches"
          // Write the default settings, and flip (0, 0) into the top-left corner
          // of the page, scale the page, then leave 0.5" margin
          buf.write("q\n" + "1 J\n" + "1 j\n" + "[] 0 d\n" + "1 w\n" + "1 0 0 -1 0 ").writes(height).write("cm\n");
          buf.writes(scale).write("0 0 ").writes(scale).writes(dpi / 2.0).writes(dpi / 2.0).write("cm\n");
          buf.write("1 0 0 1 ").writes(dpi / 2.0).writes(dpi / 2.0).write("cm\n");
      }
  
      /** Changes the color for subsequent graphical drawing. */
      public OurPDFWriter setColor(Color color) {
          int rgb = color.getRGB() & 0xFFFFFF, r = (rgb >> 16), g = (rgb >> 8) & 0xFF, b = (rgb & 0xFF);
          if (this.color == rgb)
              return this;
          else
              this.color = rgb; // no need to change
          buf.writes(r / 255.0).writes(g / 255.0).writes(b / 255.0).write("RG\n");
          buf.writes(r / 255.0).writes(g / 255.0).writes(b / 255.0).write("rg\n");
          return this;
      }
  
      /** Changes the line style to be normal. */
      public OurPDFWriter setNormalLine() {
          if (line != 0)
              buf.write("1 w [] 0 d\n");
          line = 0;
          return this;
      }
  
      /** Changes the line style to be bold. */
      public OurPDFWriter setBoldLine() {
          if (line != 1)
              buf.write("2 w [] 0 d\n");
          line = 1;
          return this;
      }
  
      /** Changes the line style to be dotted. */
      public OurPDFWriter setDottedLine() {
          if (line != 2)
              buf.write("1 w [1 3] 0 d\n");
          line = 2;
          return this;
      }
  
      /** Changes the line style to be dashed. */
      public OurPDFWriter setDashedLine() {
          if (line != 3)
              buf.write("1 w [6 3] 0 d\n");
          line = 3;
          return this;
      }
  
      /** Shifts the coordinate space by the given amount. */
      public OurPDFWriter shiftCoordinateSpace(int x, int y) {
          buf.write("1 0 0 1 ").writes(x).writes(y).write("cm\n");
          return this;
      }
  
      /** Draws a line from (x1, y1) to (x2, y2). */
      public OurPDFWriter drawLine(int x1, int y1, int x2, int y2) {
          buf.writes(x1).writes(y1).write("m ").writes(x2).writes(y2).write("l S\n");
          return this;
      }
  
      /**
       * Draws a circle of the given radius, centered at (0, 0).
       */
      public OurPDFWriter drawCircle(int radius, boolean fillOrNot) {
          double k = (0.55238 * radius); // Approximate a circle using 4 cubic
                                        // bezier curves
          buf.writes(radius).write("0 m ");
          buf.writes(radius).writes(k).writes(k).writes(radius).write("0 ").writes(radius).write("c ");
          buf.writes(-k).writes(radius).writes(-radius).writes(k).writes(-radius).write("0 c ");
          buf.writes(-radius).writes(-k).writes(-k).writes(-radius).write("0 ").writes(-radius).write("c ");
          buf.writes(k).writes(-radius).writes(radius).writes(-k).writes(radius).write(fillOrNot ? "0 c f\n" : "0 c S\n");
          return this;
      }
  
      /** Draws a shape. */
      public OurPDFWriter drawShape(Shape shape, boolean fillOrNot) {
          if (shape instanceof Polygon) {
              Polygon obj = (Polygon) shape;
              for (int i = 0; i < obj.npoints; i++)
                  buf.writes(obj.xpoints[i]).writes(obj.ypoints[i]).write(i == 0 ? "m\n" : "l\n");
              buf.write("h\n");
          } else {
              double moveX = 0, moveY = 0, nowX = 0, nowY = 0, pt[] = new double[6];
              for (PathIterator it = shape.getPathIterator(null); !it.isDone(); it.next())
                  switch (it.currentSegment(pt)) {
                      case PathIterator.SEG_MOVETO :
                          nowX = moveX = pt[0];
                          nowY = moveY = pt[1];
                          buf.writes(nowX).writes(nowY).write("m\n");
                          break;
                      case PathIterator.SEG_CLOSE :
                          nowX = moveX;
                          nowY = moveY;
                          buf.write("h\n");
                          break;
                      case PathIterator.SEG_LINETO :
                          nowX = pt[0];
                          nowY = pt[1];
                          buf.writes(nowX).writes(nowY).write("l\n");
                          break;
                      case PathIterator.SEG_CUBICTO :
                          nowX = pt[4];
                          nowY = pt[5];
                          buf.writes(pt[0]).writes(pt[1]).writes(pt[2]).writes(pt[3]).writes(nowX).writes(nowY).write("c\n");
                          break;
                      case PathIterator.SEG_QUADTO : // Convert quadratic bezier
                                                    // into cubic bezier using
                                                    // de Casteljau algorithm
                          double px = nowX + (pt[0] - nowX) * (2.0 / 3.0), qx = px + (pt[2] - nowX) / 3.0;
                          double py = nowY + (pt[1] - nowY) * (2.0 / 3.0), qy = py + (pt[3] - nowY) / 3.0;
                          nowX = pt[2];
                          nowY = pt[3];
                          buf.writes(px).writes(py).writes(qx).writes(qy).writes(nowX).writes(nowY).write("c\n");
                          break;
                  }
          }
          buf.write(fillOrNot ? "f\n" : "S\n");
          return this;
      }
  
      /*
       * PDF File Structure Summary: =========================== File should ideally
       * start with the following 13 bytes: "%PDF-1.3" 10 "%" -127 10 10 Now comes one
       * or more objects. One simple single-page arrangement is to have exactly 5
       * objects in this order: FONT, CONTENT, PAGE, PAGES, and CATALOG. Font Object
       * (1 because FONT is #1) ================================== 1 0 obj << /Type
       * /Font /Subtype /Type1 /BaseFont /Helvetica /Encoding /WinAnsiEncoding >>
       * endobj\n\n Content Object (2 because CONTENT is #2) (${LEN} is the number of
       * bytes in ${CONTENT} when compressed)
       * ========================================================= ================
       * ============================= 2 0 obj << /Length ${LEN} /Filter /FlateDecode
       * >> stream\r\n${CONTENT}endstream endobj\n\n Here is a quick summary of
       * various PDF Graphics operations
       * ========================================================= = $x $y m -->
       * begins a new path at the given coordinate $x $y l --> add the segment
       * (LASTx,LASTy)..($x,$y) to the current path $cx $cy $x $y v --> add the bezier
       * curve (LASTx,LASTy)..(LASTx,LASTy)..($cx,$cy)..($x,$y) to the current path
       * $cx $cy $x $y y --> add the bezier curve
       * (LASTx,LASTy)....($cx,$cy).....($x,$y)...($x,$y) to the current path $ax $ay
       * $bx $by $x $y c --> add the bezier curve
       * (LASTx,LASTy)....($ax,$ay)....($bx,$by)..($x,$y) to the current path h -->
       * close the current subpath by straightline segment from current point to the
       * start of this subpath $x $y $w $h re --> append a rectangle to the current
       * path as a complete subpath with lower-left corner at $x $y S --> assuming
       * we've just described a path, draw the path f --> assuming we've just
       * described a path, fill the path B --> assuming we've just described a path,
       * fill then draw the path q --> saves the current graphics state 1 J --> sets
       * the round cap 1 j --> sets the round joint [] 0 d --> sets the dash pattern
       * as SOLID [4 6] 0 d --> sets the dash pattern as 4 UNITS ON then 6 UNITS OFF 5
       * w --> sets the line width as 5 UNITS $a $b $c $d $e $f cm --> appends the
       * given matrix; for example, [1 0 0 1 dx dy] means "translation to dx dy" $R $G
       * $B RG --> sets the stroke color (where 0 <= $R <= 1, etc) $R $G $B rg -->
       * sets the fill color (where 0 <= $R <= 1, etc) Q --> restores the current
       * graphics state Page Object (3 because PAGE is #3) (4 because PAGES is #4) (2
       * because CONTENTS is #2)
       * ========================================================= ================
       * ============ 3 0 obj << /Type /Page /Parent 4 0 R /Contents 2 0 R >>
       * endobj\n\n Pages Object (4 because PAGES is #4) (3 because PAGE is #3) (${W}
       * is 8.5*DPI, ${H} is 11*DPI) (1 because FONT is #1)
       * ========================================================= ================
       * =========================================== 4 0 obj << /Type /Pages /Count 1
       * /Kids [3 0 R] /MediaBox [0 0 ${W} ${H}] /Resources << /Font << /F1 1 0 R >>
       * >> >> endobj\n\n Catalog Object (5 because CATALOG is #5) (4 because PAGES is
       * #4) ========================================================= ======= 5 0 obj
       * << /Type /Catalog /Pages 4 0 R >> endobj\n\n END_OF_FILE format (assuming we
       * have obj1 obj2 obj3 obj4 obj5 where obj5 is the "PDF Catalog")
       * ========================================================= ================
       * ===================== xref\n 0 6\n // 6 is because it's the number of objects
       * plus 1 0000000000 65535 f\r\n ${offset1} 00000 n\r\n // ${offset1} is byte
       * offset of start of obj1, left-padded-with-zero until you get exactly 10
       * digits ${offset2} 00000 n\r\n // ${offset2} is byte offset of start of obj2,
       * left-padded-with-zero until you get exactly 10 digits ${offset3} 00000 n\r\n
       * // ${offset3} is byte offset of start of obj3, left-padded-with-zero until
       * you get exactly 10 digits ${offset4} 00000 n\r\n // ${offset4} is byte offset
       * of start of obj4, left-padded-with-zero until you get exactly 10 digits
       * ${offset5} 00000 n\r\n // ${offset5} is byte offset of start of obj5,
       * left-padded-with-zero until you get exactly 10 digits trailer\n <<\n /Size
       * 6\n // 6 is because it's the number of objects plus 1 /Root 5 0 R\n // 5 is
       * because it's the Catalog Object's object ID >>\n startxref\n ${xref}\n //
       * $xref is the byte offset of the start of this entire "xref" paragraph %%EOF\n
       */
  
      /**
       * Helper method that writes the given String to the output file, then return
       * the number of bytes written.
       */
      private static int out(RandomAccessFile file, String string) throws IOException {
          byte[] array = string.getBytes("UTF-8");
          file.write(array);
          return array.length;
      }
  
      /** Close and save this PDF object. */
      public void close() throws IOException {
          if (buf == null)
              return; // already closed
          final boolean compressOrNot = true;
          RandomAccessFile out = null;
          try {
              String space = "                    "; // reserve 20 bytes for the
                                                    // file size, which is far
                                                    // far more than enough
              final long fontID = 1, contentID = 2, pageID = 3, pagesID = 4, catalogID = 5, offset[] = new long[6];
              // Write %PDF-1.3, followed by a non-ASCII comment to force the PDF
              // into binary mode
              out = new RandomAccessFile(filename, "rw");
              out.setLength(0);
              byte[] head = new byte[] {
                                        '%', 'P', 'D', 'F', '-', '1', '.', '3', 10, '%', -127, 10, 10
              };
              out.write(head);
              long now = head.length;
              // Font
              offset[1] = now;
              now += out(out, fontID + " 0 obj << /Type /Font /Subtype /Type1 /BaseFont" + " /Helvetica /Encoding /WinAnsiEncoding >> endobj\n\n");
              // Content
              offset[2] = now;
              now += out(out, contentID + " 0 obj << /Length " + space + (compressOrNot ? " /Filter /FlateDecode" : "") + " >> stream\r\n");
              buf.write("Q\n");
              final long ct = compressOrNot ? buf.dumpFlate(out) : buf.dump(out);
              now += ct + out(out, "endstream endobj\n\n");
              // Page
              offset[3] = now;
              now += out(out, pageID + " 0 obj << /Type /Page /Parent " + pagesID + " 0 R /Contents " + contentID + " 0 R >> endobj\n\n");
              // Pages
              offset[4] = now;
              now += out(out, pagesID + " 0 obj << /Type /Pages /Count 1 /Kids [" + pageID + " 0 R] /MediaBox [0 0 " + width + " " + height + "] /Resources << /Font << /F1 " + fontID + " 0 R >> >> >> endobj\n\n");
              // Catalog
              offset[5] = now;
              now += out(out, catalogID + " 0 obj << /Type /Catalog /Pages " + pagesID + " 0 R >> endobj\n\n");
              // Xref
              String xr = "xref\n" + "0 " + offset.length + "\n";
              for (int i = 0; i < offset.length; i++) {
                  String txt = Long.toString(offset[i]);
                  while (txt.length() < 10)
                      txt = "0" + txt; // must be exactly 10 characters long
                  if (i == 0)
                      xr = xr + txt + " 65535 f\r\n";
                  else
                      xr = xr + txt + " 00000 n\r\n";
              }
              // Trailer
              xr = xr + "trailer\n<<\n/Size " + offset.length + "\n/Root " + catalogID + " 0 R\n>>\n" + "startxref\n" + now + "\n%%EOF\n";
              out(out, xr);
              out.seek(offset[2]);
              out(out, contentID + " 0 obj << /Length " + ct); // move the file
                                                              // pointer back
                                                              // so we can
                                                              // write out the
                                                              // real Content
                                                              // Size
              out.close();
              buf = null; // only set buf to null if the file was saved
                         // successfully and no exception was thrown
          } catch (Throwable ex) {
              Util.close(out);
              if (ex instanceof IOException)
                  throw (IOException) ex;
              if (ex instanceof OutOfMemoryError)
                  throw new IOException("Out of memory trying to save the PDF file to " + filename);
              if (ex instanceof StackOverflowError)
                  throw new IOException("Out of memory trying to save the PDF file to " + filename);
              throw new IOException("Error writing the PDF file to " + filename + " (" + ex + ")");
          }
      }
  }
  