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