# HG changeset patch
# User wenzelm
# Date 1411650102 -7200
# Node ID 22424e43038d41315443418ab4f9fa6f4511dc24
# Parent  9c3da105db2d46551093fea90fa4a90d9951324e
save image as PNG or PDF;
more robust error dialog;

diff -r 9c3da105db2d -r 22424e43038d src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala	Thu Sep 25 12:22:12 2014 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala	Thu Sep 25 15:01:42 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))
+    }
   }
 }