src/Pure/General/graphics_file.scala
changeset 73343 d0378baf7d06
parent 73340 0ffcad1f6130
child 75393 87ebf5a50283
equal deleted inserted replaced
73342:0bf768567d9f 73343:d0378baf7d06
    61 
    61 
    62     using(new BufferedOutputStream(new FileOutputStream(file)))(out =>
    62     using(new BufferedOutputStream(new FileOutputStream(file)))(out =>
    63     {
    63     {
    64       val document = new Document()
    64       val document = new Document()
    65       try {
    65       try {
    66         document.setPageSize(new Rectangle(width, height))
    66         document.setPageSize(new Rectangle(width.toFloat, height.toFloat))
    67         val writer = PdfWriter.getInstance(document, out)
    67         val writer = PdfWriter.getInstance(document, out)
    68         document.open()
    68         document.open()
    69 
    69 
    70         val cb = writer.getDirectContent()
    70         val cb = writer.getDirectContent()
    71         val tp = cb.createTemplate(width, height)
    71         val tp = cb.createTemplate(width.toFloat, height.toFloat)
    72         val gfx = tp.createGraphics(width, height, font_mapper())
    72         val gfx = tp.createGraphics(width.toFloat, height.toFloat, font_mapper())
    73 
    73 
    74         paint(gfx)
    74         paint(gfx)
    75         gfx.dispose
    75         gfx.dispose
    76 
    76 
    77         cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
    77         cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)