--- a/src/Pure/build-jars Sun Jan 18 17:32:38 2015 +0100
+++ b/src/Pure/build-jars Sun Jan 18 17:34:14 2015 +0100
@@ -109,11 +109,12 @@
"../Tools/Graphview/main_panel.scala"
"../Tools/Graphview/metrics.scala"
"../Tools/Graphview/model.scala"
+ "../Tools/Graphview/mutator.scala"
"../Tools/Graphview/mutator_dialog.scala"
"../Tools/Graphview/mutator_event.scala"
- "../Tools/Graphview/mutator.scala"
"../Tools/Graphview/popups.scala"
"../Tools/Graphview/shapes.scala"
+ "../Tools/Graphview/tree_panel.scala"
"../Tools/Graphview/visualizer.scala"
)
--- a/src/Tools/Graphview/graph_panel.scala Sun Jan 18 17:32:38 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Sun Jan 18 17:34:14 2015 +0100
@@ -36,9 +36,6 @@
}
}
- focusable = true
- requestFocus()
-
horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
@@ -67,12 +64,6 @@
refresh()
}
- def apply_layout()
- {
- visualizer.update_layout()
- refresh()
- }
-
private class Paint_Panel extends Panel
{
def set_preferred_size()
@@ -112,7 +103,6 @@
visualizer.model.Colors.events += { case _ => repaint() }
visualizer.model.Mutators.events += { case _ => repaint() }
- apply_layout()
rescale(1.0)
private object Transform
--- a/src/Tools/Graphview/main_panel.scala Sun Jan 18 17:32:38 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Sun Jan 18 17:34:14 2015 +0100
@@ -10,7 +10,7 @@
import isabelle._
-import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser}
+import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, SplitPane, Orientation}
import java.io.{File => JFile}
import java.awt.{Color, Graphics2D}
@@ -21,13 +21,20 @@
class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel
{
- focusable = true
- requestFocus()
+ private def repaint_graph() { if (graph_panel != null) graph_panel.repaint }
val graph_panel = new Graph_Panel(visualizer)
+ val tree_panel = new Tree_Panel(visualizer, repaint_graph _)
- listenTo(keys)
- reactions += graph_panel.reactions
+ def update_layout()
+ {
+ visualizer.update_layout()
+ tree_panel.refresh()
+ graph_panel.refresh()
+ }
+
+ val split_pane = new SplitPane(Orientation.Vertical, tree_panel, graph_panel)
+ split_pane.oneTouchExpandable = true
val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)
@@ -37,31 +44,35 @@
chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
chooser.title = "Save image (.png or .pdf)"
- val options_panel =
+ val controls =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
new CheckBox() {
+ tooltip = "Show full node content"
selected = visualizer.show_content
action = Action("Show content") {
visualizer.show_content = selected
- graph_panel.apply_layout()
+ update_layout()
}
},
new CheckBox() {
+ tooltip = "Draw edges with explicit arrow heads"
selected = visualizer.show_arrow_heads
action = Action("Show arrow heads") {
visualizer.show_arrow_heads = selected
- graph_panel.repaint()
+ repaint_graph()
}
},
new CheckBox() {
+ tooltip = "Show dummy nodes -- easier mouse dragging"
selected = visualizer.show_dummies
action = Action("Show dummies") {
visualizer.show_dummies = selected
- graph_panel.repaint()
+ repaint_graph()
}
},
new Button {
action = Action("Save image") {
+ tooltip = "Save current image as PNG or PDF"
chooser.showSaveDialog(this) match {
case FileChooser.Result.Approve => export(chooser.selectedFile)
case _ =>
@@ -70,12 +81,13 @@
},
graph_panel.zoom,
new Button { action = Action("Fit to window") { graph_panel.fit_to_window() } },
- new Button { action = Action("Apply layout") { graph_panel.apply_layout() } },
+ new Button { action = Action("Update layout") { update_layout() } },
new Button { action = Action("Colorations") { color_dialog.open } },
new Button { action = Action("Filters") { mutator_dialog.open } })
- add(graph_panel, BorderPanel.Position.Center)
- add(options_panel, BorderPanel.Position.North)
+ layout(split_pane) = BorderPanel.Position.Center
+ layout(controls) = BorderPanel.Position.North
+ update_layout()
private def export(file: JFile)
{
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/tree_panel.scala Sun Jan 18 17:34:14 2015 +0100
@@ -0,0 +1,163 @@
+/* Title: Tools/Graphview/tree_panel.scala
+ Author: Makarius
+
+Tree view on graph nodes.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.Dimension
+import java.awt.event.{MouseEvent, MouseAdapter}
+import javax.swing.JTree
+import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
+import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener,
+ DocumentListener, DocumentEvent}
+
+import scala.util.matching.Regex
+import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button,
+ CheckBox, Action}
+
+
+class Tree_Panel(val visualizer: Visualizer, repaint_graph: () => Unit) extends BorderPanel
+{
+ /* tree */
+
+ private var nodes = List.empty[Graph_Display.Node]
+ private val root = new DefaultMutableTreeNode("Nodes")
+
+ private val tree = new JTree(root)
+ tree.addMouseListener(new MouseAdapter {
+ override def mouseClicked(e: MouseEvent)
+ {
+ val click = tree.getPathForLocation(e.getX, e.getY)
+ if (click != null && e.getClickCount == 1) {
+ (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
+ case (tree_node: DefaultMutableTreeNode, tree_node1: DefaultMutableTreeNode)
+ if tree_node == tree_node1 =>
+ tree_node.getUserObject match {
+ case node: Graph_Display.Node => visualizer.current_node = Some(node)
+ case _ => visualizer.current_node = None
+ }
+ case _ => visualizer.current_node = None
+ }
+ repaint_graph()
+ }
+ }
+ })
+
+ private val tree_pane = new ScrollPane(Component.wrap(tree))
+ tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
+ tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
+ tree_pane.minimumSize = new Dimension(100, 50)
+ tree_pane.peer.getVerticalScrollBar.setUnitIncrement(10)
+
+
+ /* controls */
+
+ private val alphabetic = new CheckBox {
+ tooltip = "Alphabetic order instead of topological order"
+ selected = visualizer.alphabetic_order
+ action = Action("Alphabetic order") {
+ visualizer.alphabetic_order = selected
+ refresh()
+ }
+ }
+
+ private var selection_pattern: Option[Regex] = None
+
+ private def selection_filter(node: Graph_Display.Node): Boolean =
+ selection_pattern match {
+ case None => true
+ case Some(re) => re.pattern.matcher(node.toString).find
+ }
+
+ private val selection_label = new Label("Selection:") {
+ tooltip = "Selection of nodes via regular expression"
+ }
+
+ private val selection_field = new TextField(10) {
+ tooltip = selection_label.tooltip
+ }
+ private val selection_field_foreground = selection_field.foreground
+
+ private val selection_delay =
+ GUI_Thread.delay_last(visualizer.get_options.seconds("editor_input_delay")) {
+ val (pattern, ok) =
+ selection_field.text match {
+ case null | "" => (None, true)
+ case s =>
+ val pattern = Library.make_regex(s)
+ (pattern, pattern.isDefined)
+ }
+ if (selection_pattern != pattern) {
+ selection_pattern = pattern
+ // FIXME
+ System.console.writer.println(pattern)
+ }
+ selection_field.foreground =
+ if (ok) selection_field_foreground else visualizer.error_color
+ }
+
+ selection_field.peer.getDocument.addDocumentListener(new DocumentListener {
+ def changedUpdate(e: DocumentEvent) { selection_delay.invoke() }
+ def insertUpdate(e: DocumentEvent) { selection_delay.invoke() }
+ def removeUpdate(e: DocumentEvent) { selection_delay.invoke() }
+ })
+
+ private val selection_apply = new Button {
+ tooltip = "Apply tree selection to graph"
+ action = Action("<html><b>Apply</b></html>") {
+ visualizer.current_node = None
+ visualizer.Selection.clear()
+ val paths = tree.getSelectionPaths
+ if (paths != null) {
+ for (path <- paths) {
+ path.getLastPathComponent match {
+ case tree_node: DefaultMutableTreeNode =>
+ tree_node.getUserObject match {
+ case node: Graph_Display.Node => visualizer.Selection.add(node)
+ case _ =>
+ }
+ case _ =>
+ }
+ }
+ }
+ repaint_graph()
+ }
+ }
+
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ alphabetic, selection_label, selection_field, selection_apply)
+
+
+ /* main layout */
+
+ def refresh()
+ {
+ val new_nodes =
+ if (visualizer.alphabetic_order)
+ visualizer.visible_graph.keys_iterator.toList
+ else
+ visualizer.visible_graph.topological_order
+
+ if (new_nodes != nodes) {
+ nodes = new_nodes
+
+ root.removeAllChildren
+ for (node <- nodes) root.add(new DefaultMutableTreeNode(node))
+
+ tree.clearSelection
+ for (i <- 0 until tree.getRowCount) tree.expandRow(i)
+ tree.revalidate()
+ }
+ revalidate()
+ repaint()
+ }
+
+ layout(tree_pane) = BorderPanel.Position.Center
+ layout(controls) = BorderPanel.Position.North
+ refresh()
+}
--- a/src/Tools/Graphview/visualizer.scala Sun Jan 18 17:32:38 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala Sun Jan 18 17:34:14 2015 +0100
@@ -20,6 +20,9 @@
visualizer =>
+ def get_options: Options = options
+
+
/* layout state */
// owned by GUI thread
@@ -91,6 +94,7 @@
def foreground_color: Color = Color.BLACK
def background_color: Color = Color.WHITE
def selection_color: Color = Color.GREEN
+ def current_color: Color = Color.YELLOW
def error_color: Color = Color.RED
def dummy_color: Color = Color.GRAY
@@ -141,6 +145,9 @@
Shapes.paint_node(gfx, visualizer, node)
}
+ var alphabetic_order: Boolean = false
+ var current_node: Option[Graph_Display.Node] = None
+
object Selection
{
// owned by GUI thread
@@ -156,7 +163,9 @@
sealed case class Node_Color(border: Color, background: Color, foreground: Color)
def node_color(node: Graph_Display.Node): Node_Color =
- if (Selection.contains(node))
+ if (current_node == Some(node))
+ Node_Color(foreground_color, current_color, foreground_color)
+ else if (Selection.contains(node))
Node_Color(foreground_color, selection_color, foreground_color)
else
Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sun Jan 18 17:32:38 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sun Jan 18 17:34:14 2015 +0100
@@ -76,6 +76,7 @@
override def foreground_color = view.getTextArea.getPainter.getForeground
override def background_color = view.getTextArea.getPainter.getBackground
override def selection_color = view.getTextArea.getPainter.getSelectionColor
+ override def current_color = view.getTextArea.getPainter.getLineHighlightColor
override def error_color = PIDE.options.color_value("error_color")
override def make_font(): Font =
@@ -97,7 +98,7 @@
GUI_Thread.later {
graphview match {
case main_panel: isabelle.graphview.Main_Panel =>
- main_panel.graph_panel.apply_layout()
+ main_panel.update_layout()
case _ =>
}
}