merged

--- a/Admin/isatest/settings/at-poly	Thu Sep 25 16:35:56 2014 +0200
+++ b/Admin/isatest/settings/at-poly	Thu Sep 25 17:07:44 2014 +0200
@@ -28,3 +28,11 @@
 
 ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
 
+ISABELLE_GHC=ghc
+#ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/home/smlnj/bin/sml"
+

--- a/src/Pure/General/graphics_file.scala	Thu Sep 25 16:35:56 2014 +0200
+++ b/src/Pure/General/graphics_file.scala	Thu Sep 25 17:07:44 2014 +0200
@@ -7,15 +7,36 @@
 package isabelle
 
 
+import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
 import java.awt.Graphics2D
 import java.awt.geom.Rectangle2D
-import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
+import java.awt.image.BufferedImage
+import javax.imageio.ImageIO
 
 import org.jfree.chart.JFreeChart
 
 
 object Graphics_File
 {
+  /* PNG */
+
+  def write_png(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72)
+  {
+    val scale = dpi / 72.0f
+    val w = (width * scale).round
+    val h = (height * scale).round
+
+    val img = new BufferedImage(w, h, BufferedImage.TYPE_INT_ARGB)
+    val gfx = img.createGraphics
+    try {
+      gfx.scale(scale, scale)
+      paint(gfx)
+      ImageIO.write(img, "png", file)
+    }
+    finally { gfx.dispose }
+  }
+
+
   /* PDF */
 
   def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)

--- a/src/Tools/Graphview/src/main_panel.scala	Thu Sep 25 16:35:56 2014 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala	Thu Sep 25 17:07:44 2014 +0200
@@ -14,8 +14,8 @@
 import scala.swing.{BorderPanel, Button, BoxPanel,
   Orientation, Swing, CheckBox, Action, FileChooser}
 
-import java.io.File
-import java.awt.{Color, Dimension}
+import java.io.{File => JFile}
+import java.awt.{Color, Dimension, Graphics2D}
 import java.awt.geom.Rectangle2D
 import java.awt.image.BufferedImage
 import javax.imageio.ImageIO
@@ -23,8 +23,7 @@
 import javax.swing.JComponent
 
 
-class Main_Panel(graph: Model.Graph)
-  extends BorderPanel
+class Main_Panel(graph: Model.Graph) extends BorderPanel
 {
   focusable = true
   requestFocus()
@@ -44,7 +43,7 @@
 
   private val chooser = new FileChooser()
   chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
-  chooser.title = "Graph export"
+  chooser.title = "Save Image (.png or .pdf)"
 
   val options_panel = new BoxPanel(Orientation.Horizontal) {
     border = new EmptyBorder(0, 0, 10, 0)
@@ -59,7 +58,7 @@
     }
     contents += Swing.RigidBox(new Dimension(10, 0))
     contents += new Button{
-      action = Action("Save as PNG"){
+      action = Action("Save Image"){
         chooser.showSaveDialog(this) match {
           case FileChooser.Result.Approve => export(chooser.selectedFile)
           case _ =>
@@ -98,20 +97,29 @@
   add(graph_panel, BorderPanel.Position.Center)
   add(options_panel, BorderPanel.Position.North)
 
-  private def export(file: File) {
-    val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
-    val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
-                                (math.abs(maxY - minY) + 200).toInt,
-                                BufferedImage.TYPE_INT_RGB)
-    val g = img.createGraphics
-    g.setColor(Color.WHITE)
-    g.fill(new Rectangle2D.Double(0, 0, img.getWidth(), img.getHeight()))
+  private def export(file: JFile)
+  {
+    val (x0, y0, x1, y1) = visualizer.Coordinates.bounds
+    val w = (math.abs(x1 - x0) + 400).toInt
+    val h = (math.abs(y1 - y0) + 200).toInt
+
+    def paint(gfx: Graphics2D)
+    {
+      gfx.setColor(Color.WHITE)
+      gfx.fill(new Rectangle2D.Double(0, 0, w, h))
 
-    g.translate(- minX + 200, - minY + 100)
-    visualizer.Drawer.paint_all_visible(g, false)
-    g.dispose()
+      gfx.translate(- x0 + 200, - y0 + 100)
+      visualizer.Drawer.paint_all_visible(gfx, false)
+    }
 
-    try { ImageIO.write(img, "png", file) }
-    catch { case ex: Exception => ex.printStackTrace }  // FIXME !?
+    try {
+      val name = file.getName
+      if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
+      else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
+      else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
+    }
+    catch {
+      case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
+    }
   }
 }