# HG changeset patch # User wenzelm # Date 1421598854 -3600 # Node ID 02bacfc31446a4903339a7b06c34f63a8da78b0e # Parent 39a38657d16b0816f30a835a62cc6f135eb51f02 support for tree view on graph nodes; misc tuning; diff -r 39a38657d16b -r 02bacfc31446 src/Pure/build-jars --- 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" ) diff -r 39a38657d16b -r 02bacfc31446 src/Tools/Graphview/graph_panel.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 diff -r 39a38657d16b -r 02bacfc31446 src/Tools/Graphview/main_panel.scala --- 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) { diff -r 39a38657d16b -r 02bacfc31446 src/Tools/Graphview/tree_panel.scala --- /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("Apply") { + 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() +} diff -r 39a38657d16b -r 02bacfc31446 src/Tools/Graphview/visualizer.scala --- 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) diff -r 39a38657d16b -r 02bacfc31446 src/Tools/jEdit/src/graphview_dockable.scala --- 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 _ => } }