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