src/Pure/General/graphics_file.scala
changeset 65862 5441c51a2d38
parent 65086 548efa2bda66
child 65999 ee4cf96a9406
equal deleted inserted replaced
65861:f35abc25d7b1 65862:5441c51a2d38
    53       mapper.putName(name, parameters)
    53       mapper.putName(name, parameters)
    54     }
    54     }
    55     mapper
    55     mapper
    56   }
    56   }
    57 
    57 
    58   def write_pdf(
    58   def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)
    59     file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)
       
    60   {
    59   {
    61     import com.lowagie.text.{Document, Rectangle}
    60     import com.lowagie.text.{Document, Rectangle}
    62 
    61 
    63     val out = new BufferedOutputStream(new FileOutputStream(file))
    62     val out = new BufferedOutputStream(new FileOutputStream(file))
    64     try {
    63     try {
    80       finally { document.close() }
    79       finally { document.close() }
    81     }
    80     }
    82     finally { out.close }
    81     finally { out.close }
    83   }
    82   }
    84 
    83 
    85   def write_pdf(path: Path, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
       
    86     write_pdf(path.file, paint, width, height)
       
    87 
    84 
    88   def write_pdf(file: JFile, chart: JFreeChart, width: Int, height: Int)
    85   /* JFreeChart */
    89   {
       
    90     def paint(gfx: Graphics2D) = chart.draw(gfx, new Rectangle2D.Double(0, 0, width, height))
       
    91     write_pdf(file, paint _, width, height)
       
    92   }
       
    93 
    86 
    94   def write_pdf(path: Path, chart: JFreeChart, width: Int, height: Int): Unit =
    87   def paint_chart(gfx: Graphics2D, chart: JFreeChart, width: Int, height: Int): Unit =
    95     write_pdf(path.file, chart, width, height)
    88     chart.draw(gfx, new Rectangle2D.Double(0, 0, width, height))
       
    89 
       
    90   def write_chart_png(file: JFile, chart: JFreeChart, width: Int, height: Int): Unit =
       
    91     write_png(file, paint_chart(_, chart, width, height), width, height)
       
    92 
       
    93   def write_chart_pdf(file: JFile, chart: JFreeChart, width: Int, height: Int): Unit =
       
    94     write_pdf(file, paint_chart(_, chart, width, height), width, height)
    96 }
    95 }