src/Tools/Graphview/src/main_panel.scala
author wenzelm
Wed May 21 12:49:27 2014 +0200 (2014-05-21)
changeset 57035 e865c4d99c49
parent 50491 0faaa279faee
child 57044 042d6e58cb40
permissions -rw-r--r--
unused;
     1 /*  Title:      Tools/Graphview/src/main_panel.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3 
     4 Graph Panel wrapper.
     5 */
     6 
     7 package isabelle.graphview
     8 
     9 
    10 import isabelle._
    11 import isabelle.graphview.Mutators._
    12 
    13 import scala.collection.JavaConversions._
    14 import scala.swing.{BorderPanel, Button, BoxPanel,
    15   Orientation, Swing, CheckBox, Action, FileChooser}
    16 
    17 import java.io.File
    18 import java.awt.{Color, Dimension}
    19 import java.awt.geom.Rectangle2D
    20 import java.awt.image.BufferedImage
    21 import javax.imageio.ImageIO
    22 import javax.swing.border.EmptyBorder
    23 import javax.swing.JComponent
    24 
    25 
    26 class Main_Panel(graph: Model.Graph)
    27   extends BorderPanel
    28 {
    29   focusable = true
    30   requestFocus()
    31 
    32   val model = new Model(graph)
    33   val visualizer = new Visualizer(model)
    34 
    35   def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
    36   val graph_panel = new Graph_Panel(visualizer, make_tooltip)
    37 
    38   listenTo(keys)
    39   reactions += graph_panel.reactions
    40 
    41   val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)
    42 
    43   val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations")
    44 
    45   private val chooser = new FileChooser()
    46   chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
    47   chooser.title = "Graph export"
    48 
    49   val options_panel = new BoxPanel(Orientation.Horizontal) {
    50     border = new EmptyBorder(0, 0, 10, 0)
    51 
    52     contents += Swing.HGlue
    53     contents += new CheckBox(){
    54       selected = visualizer.arrow_heads
    55       action = Action("Arrow Heads"){
    56         visualizer.arrow_heads = selected
    57         graph_panel.repaint()
    58       }
    59     }
    60     contents += Swing.RigidBox(new Dimension(10, 0))
    61     contents += new Button{
    62       action = Action("Save as PNG"){
    63         chooser.showSaveDialog(this) match {
    64           case FileChooser.Result.Approve => export(chooser.selectedFile)
    65           case _ =>
    66         }
    67       }
    68     }
    69     contents += Swing.RigidBox(new Dimension(10, 0))
    70     contents += graph_panel.zoom_box
    71 
    72     contents += Swing.RigidBox(new Dimension(10, 0))
    73     contents += new Button{
    74       action = Action("Apply Layout"){
    75         graph_panel.apply_layout()
    76       }
    77     }
    78     contents += Swing.RigidBox(new Dimension(10, 0))
    79     contents += new Button{
    80       action = Action("Fit to Window"){
    81         graph_panel.fit_to_window()
    82       }
    83     }
    84     contents += Swing.RigidBox(new Dimension(10, 0))
    85     contents += new Button{
    86       action = Action("Colorations"){
    87         color_dialog.open
    88       }
    89     }
    90     contents += Swing.RigidBox(new Dimension(10, 0))
    91     contents += new Button{
    92       action = Action("Filters"){
    93         mutator_dialog.open
    94       }
    95     }
    96   }
    97 
    98   add(graph_panel, BorderPanel.Position.Center)
    99   add(options_panel, BorderPanel.Position.North)
   100 
   101   private def export(file: File) {
   102     val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
   103     val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
   104                                 (math.abs(maxY - minY) + 200).toInt,
   105                                 BufferedImage.TYPE_INT_RGB)
   106     val g = img.createGraphics
   107     g.setColor(Color.WHITE)
   108     g.fill(new Rectangle2D.Double(0, 0, img.getWidth(), img.getHeight()))
   109 
   110     g.translate(- minX + 200, - minY + 100)
   111     visualizer.Drawer.paint_all_visible(g, false)
   112     g.dispose()
   113 
   114     try { ImageIO.write(img, "png", file) }
   115     catch { case ex: Exception => ex.printStackTrace }  // FIXME !?
   116   }
   117 }