diff -r 0bf768567d9f -r d0378baf7d06 src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Mon Mar 01 22:37:33 2021 +0100
+++ b/src/Pure/General/graphics_file.scala	Mon Mar 01 22:50:00 2021 +0100
@@ -63,13 +63,13 @@
     {
       val document = new Document()
       try {
-        document.setPageSize(new Rectangle(width, height))
+        document.setPageSize(new Rectangle(width.toFloat, height.toFloat))
         val writer = PdfWriter.getInstance(document, out)
         document.open()
 
         val cb = writer.getDirectContent()
-        val tp = cb.createTemplate(width, height)
-        val gfx = tp.createGraphics(width, height, font_mapper())
+        val tp = cb.createTemplate(width.toFloat, height.toFloat)
+        val gfx = tp.createGraphics(width.toFloat, height.toFloat, font_mapper())
 
         paint(gfx)
         gfx.dispose