--- /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()
+}