1.1 --- a/src/Tools/Graphview/src/main_panel.scala	Mon Oct 08 14:10:38 2012 +0200
     1.2 +++ b/src/Tools/Graphview/src/main_panel.scala	Mon Oct 08 14:49:04 2012 +0200
     1.3 @@ -14,10 +14,13 @@
     1.4  import scala.swing.{BorderPanel, Button, BoxPanel,
     1.5    Orientation, Swing, CheckBox, Action, FileChooser}
     1.6  
     1.7 +import java.io.File
     1.8 +import java.awt.{Color, Dimension}
     1.9 +import java.awt.geom.Rectangle2D
    1.10 +import java.awt.image.BufferedImage
    1.11 +import javax.imageio.ImageIO
    1.12  import javax.swing.border.EmptyBorder
    1.13  import javax.swing.JComponent
    1.14 -import java.awt.Dimension
    1.15 -import java.io.File
    1.16  
    1.17  
    1.18  class Main_Panel(graph: Model.Graph)
    1.19 @@ -115,11 +118,6 @@
    1.20    add(options_panel, BorderPanel.Position.North)
    1.21    
    1.22    private def export(file: File) {
    1.23 -    import java.awt.image.BufferedImage
    1.24 -    import javax.imageio.ImageIO
    1.25 -    import java.awt.geom.Rectangle2D
    1.26 -    import java.awt.Color    
    1.27 -    
    1.28      val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
    1.29      val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
    1.30                                  (math.abs(maxY - minY) + 200).toInt,
    1.31 @@ -132,10 +130,7 @@
    1.32      visualizer.Drawer.paint_all_visible(g, false)
    1.33      g.dispose()    
    1.34      
    1.35 -    try {
    1.36 -      ImageIO.write(img, "png", file)
    1.37 -    } catch {
    1.38 -      case ex: Exception => ex.printStackTrace
    1.39 -    }  
    1.40 +    try { ImageIO.write(img, "png", file) }
    1.41 +    catch { case ex: Exception => ex.printStackTrace }  // FIXME !?
    1.42    }
    1.43  }