# HG changeset patch
# User wenzelm
# Date 1422204494 -3600
# Node ID ab2c3597f1d3924b16ca67ef89e2a3ca95261e16
# Parent  07e3c15cb10cd493998f7718bdb6a37a27c0576b
separate module Graph_File;

diff -r 07e3c15cb10c -r ab2c3597f1d3 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Jan 25 17:17:37 2015 +0100
+++ b/src/Pure/build-jars	Sun Jan 25 17:48:14 2015 +0100
@@ -104,6 +104,7 @@
   library.scala
   term.scala
   term_xml.scala
+  "../Tools/Graphview/graph_file.scala"
   "../Tools/Graphview/graph_panel.scala"
   "../Tools/Graphview/layout.scala"
   "../Tools/Graphview/main_panel.scala"
diff -r 07e3c15cb10c -r ab2c3597f1d3 src/Tools/Graphview/graph_file.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/graph_file.scala	Sun Jan 25 17:48:14 2015 +0100
@@ -0,0 +1,37 @@
+/*  Title:      Tools/Graphview/graph_file.scala
+    Author:     Makarius
+
+File system operations for graph output.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.io.{File => JFile}
+import java.awt.{Color, Graphics2D}
+
+
+object Graph_File
+{
+  def write(visualizer: Visualizer, file: JFile)
+  {
+    val box = visualizer.bounding_box()
+    val w = box.width.ceil.toInt
+    val h = box.height.ceil.toInt
+
+    def paint(gfx: Graphics2D)
+    {
+      gfx.setColor(Color.WHITE)
+      gfx.fillRect(0, 0, w, h)
+      gfx.translate(- box.x, - box.y)
+      visualizer.paint_all_visible(gfx)
+    }
+
+    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)")
+  }
+}
diff -r 07e3c15cb10c -r ab2c3597f1d3 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Sun Jan 25 17:17:37 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sun Jan 25 17:48:14 2015 +0100
@@ -10,8 +10,7 @@
 
 import isabelle._
 
-import java.io.{File => JFile}
-import java.awt.{Color, Dimension, Graphics2D, Point, Rectangle}
+import java.awt.{Dimension, Graphics2D, Point, Rectangle}
 import java.awt.geom.{AffineTransform, Point2D}
 import javax.imageio.ImageIO
 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
@@ -306,7 +305,11 @@
   private val save_image = new Button {
     action = Action("Save image") {
       chooser.showSaveDialog(this) match {
-        case FileChooser.Result.Approve => save_file(chooser.selectedFile)
+        case FileChooser.Result.Approve =>
+          try { Graph_File.write(visualizer, chooser.selectedFile) }
+          catch {
+            case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
+          }
         case _ =>
       }
     }
@@ -336,34 +339,6 @@
       save_image, zoom, fit_window, update_layout) // FIXME colorations, filters
 
 
-  /* save file */
-
-  private def save_file(file: JFile)
-  {
-    val box = visualizer.bounding_box()
-    val w = box.width.ceil.toInt
-    val h = box.height.ceil.toInt
-
-    def paint(gfx: Graphics2D)
-    {
-      gfx.setColor(Color.WHITE)
-      gfx.fillRect(0, 0, w, h)
-      gfx.translate(- box.x, - box.y)
-      visualizer.paint_all_visible(gfx)
-    }
-
-    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))
-    }
-  }
-
-
 
   /** main layout **/