src/Tools/Graphview/tree_panel.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 66206 2d2082db735a
permissions -rw-r--r--
more strict AFP properties;
     1 /*  Title:      Tools/Graphview/tree_panel.scala
     2     Author:     Makarius
     3 
     4 Tree view on graph nodes.
     5 */
     6 
     7 package isabelle.graphview
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Dimension, Rectangle}
    13 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
    14 import javax.swing.JTree
    15 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel, TreePath}
    16 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
    17 
    18 import scala.util.matching.Regex
    19 import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, CheckBox, Action}
    20 
    21 
    22 class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel) extends BorderPanel
    23 {
    24   /* main actions */
    25 
    26   private def selection_action()
    27   {
    28     if (tree != null) {
    29       graphview.current_node = None
    30       graphview.Selection.clear()
    31       val paths = tree.getSelectionPaths
    32       if (paths != null) {
    33         for (path <- paths if path != null) {
    34           path.getLastPathComponent match {
    35             case tree_node: DefaultMutableTreeNode =>
    36               tree_node.getUserObject match {
    37                 case node: Graph_Display.Node => graphview.Selection.add(node)
    38                 case _ =>
    39               }
    40             case _ =>
    41           }
    42         }
    43       }
    44       graph_panel.repaint()
    45     }
    46   }
    47 
    48   private def point_action(path: TreePath)
    49   {
    50     if (tree_pane != null && path != null) {
    51       val action_node =
    52         path.getLastPathComponent match {
    53           case tree_node: DefaultMutableTreeNode =>
    54             tree_node.getUserObject match {
    55               case node: Graph_Display.Node => Some(node)
    56               case _ => None
    57             }
    58           case _ => None
    59         }
    60       action_node.foreach(graph_panel.scroll_to_node(_))
    61       graphview.current_node = action_node
    62       graph_panel.repaint()
    63     }
    64   }
    65 
    66 
    67   /* tree */
    68 
    69   private var nodes = List.empty[Graph_Display.Node]
    70   private val root = new DefaultMutableTreeNode("Nodes")
    71 
    72   val tree = new JTree(root)
    73   tree.setRowHeight(0)
    74 
    75   tree.addKeyListener(new KeyAdapter {
    76     override def keyPressed(e: KeyEvent): Unit =
    77       if (e.getKeyCode == KeyEvent.VK_ENTER) {
    78         e.consume
    79         selection_action()
    80       }
    81   })
    82   tree.addMouseListener(new MouseAdapter {
    83     override def mousePressed(e: MouseEvent): Unit =
    84       if (e.getClickCount == 2)
    85         point_action(tree.getPathForLocation(e.getX, e.getY))
    86   })
    87 
    88   private val tree_pane = new ScrollPane(Component.wrap(tree))
    89   tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
    90   tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
    91   tree_pane.minimumSize = new Dimension(200, 100)
    92   tree_pane.peer.getVerticalScrollBar.setUnitIncrement(10)
    93 
    94 
    95   /* controls */
    96 
    97   private var selection_pattern: Option[Regex] = None
    98 
    99   private def selection_filter(node: Graph_Display.Node): Boolean =
   100     selection_pattern match {
   101       case None => false
   102       case Some(re) => re.pattern.matcher(node.toString).find
   103     }
   104 
   105   private val selection_label = new Label("Selection:") {
   106     tooltip = "Selection of nodes via regular expression"
   107   }
   108 
   109   private val selection_field = new TextField(10) {
   110     tooltip = selection_label.tooltip
   111   }
   112   private val selection_field_foreground = selection_field.foreground
   113 
   114   private val selection_delay =
   115     GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) {
   116       val (pattern, ok) =
   117         selection_field.text match {
   118           case null | "" => (None, true)
   119           case s =>
   120             val pattern = Library.make_regex(s)
   121             (pattern, pattern.isDefined)
   122         }
   123       if (selection_pattern != pattern) {
   124         selection_pattern = pattern
   125         tree.setSelectionRows(
   126           (for { (node, i) <- nodes.iterator.zipWithIndex if selection_filter(node) }
   127             yield i + 1).toArray)
   128         tree.repaint()
   129       }
   130       selection_field.foreground =
   131         if (ok) selection_field_foreground else graphview.error_color
   132     }
   133 
   134   selection_field.peer.getDocument.addDocumentListener(new DocumentListener {
   135     def changedUpdate(e: DocumentEvent) { selection_delay.invoke() }
   136     def insertUpdate(e: DocumentEvent) { selection_delay.invoke() }
   137     def removeUpdate(e: DocumentEvent) { selection_delay.invoke() }
   138   })
   139 
   140   private val selection_apply = new Button {
   141     action = Action("<html><b>Apply</b></html>") { selection_action () }
   142     tooltip = "Apply tree selection to graph"
   143   }
   144 
   145   private val controls =
   146     Wrap_Panel(List(selection_label, selection_field, selection_apply))
   147 
   148 
   149   /* main layout */
   150 
   151   def refresh()
   152   {
   153     val new_nodes = graphview.visible_graph.topological_order
   154     if (new_nodes != nodes) {
   155       tree.clearSelection
   156 
   157       nodes = new_nodes
   158 
   159       root.removeAllChildren
   160       for (node <- nodes) root.add(new DefaultMutableTreeNode(node))
   161 
   162       tree.expandRow(0)
   163       tree.revalidate()
   164     }
   165     revalidate()
   166     repaint()
   167   }
   168 
   169   layout(tree_pane) = BorderPanel.Position.Center
   170   layout(controls) = BorderPanel.Position.North
   171   refresh()
   172 }