src/Tools/Graphview/popups.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 59459 985fc55e9f27
permissions -rw-r--r--
more strict AFP properties;
wenzelm@59202
     1
/*  Title:      Tools/Graphview/popups.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
wenzelm@59240
     3
    Author:     Makarius
markus@49557
     4
markus@49557
     5
PopupMenu generation for graph components.
markus@49557
     6
*/
markus@49557
     7
markus@49557
     8
package isabelle.graphview
markus@49557
     9
markus@49557
    10
markus@49557
    11
import isabelle._
wenzelm@55618
    12
markus@49557
    13
import javax.swing.JPopupMenu
wenzelm@49558
    14
import scala.swing.{Action, Menu, MenuItem, Separator}
markus@49557
    15
markus@49557
    16
wenzelm@50472
    17
object Popups
wenzelm@50472
    18
{
wenzelm@59245
    19
  def apply(
wenzelm@59408
    20
    graph_panel: Graph_Panel,
wenzelm@59245
    21
    mouse_node: Option[Graph_Display.Node],
wenzelm@59245
    22
    selected_nodes: List[Graph_Display.Node]): JPopupMenu =
markus@49557
    23
  {
wenzelm@59459
    24
    val graphview = graph_panel.graphview
wenzelm@50472
    25
wenzelm@59459
    26
    val add_mutator = graphview.model.Mutators.add _
wenzelm@59459
    27
    val visible_graph = graphview.visible_graph
wenzelm@50472
    28
wenzelm@59245
    29
    def filter_context(
wenzelm@59245
    30
        nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =
markus@49557
    31
      new Menu(caption) {
wenzelm@59218
    32
        contents +=
wenzelm@59218
    33
          new MenuItem(new Action("This") {
markus@49557
    34
            def apply =
wenzelm@59459
    35
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, false)))
markus@49557
    36
          })
markus@49557
    37
wenzelm@59218
    38
        contents +=
wenzelm@59218
    39
          new MenuItem(new Action("Family") {
markus@49557
    40
            def apply =
wenzelm@59459
    41
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, true)))
markus@49557
    42
          })
markus@49557
    43
wenzelm@59218
    44
        contents +=
wenzelm@59218
    45
          new MenuItem(new Action("Parents") {
markus@49557
    46
            def apply =
wenzelm@59459
    47
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, true)))
markus@49557
    48
          })
markus@49557
    49
wenzelm@59218
    50
        contents +=
wenzelm@59218
    51
          new MenuItem(new Action("Children") {
markus@49557
    52
            def apply =
wenzelm@59459
    53
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, false)))
markus@49557
    54
          })
markus@49557
    55
markus@49557
    56
        if (edges) {
wenzelm@59256
    57
          def degree_nodes(succs: Boolean) =
wenzelm@59256
    58
            (for {
wenzelm@59256
    59
              from <- nodes.iterator
wenzelm@59259
    60
              tos = if (succs) visible_graph.imm_succs(from) else visible_graph.imm_preds(from)
wenzelm@59256
    61
              if tos.nonEmpty
wenzelm@59256
    62
            } yield (from, tos)).toList.sortBy(_._1)(Graph_Display.Node.Ordering)
wenzelm@59256
    63
wenzelm@59256
    64
          val outs = degree_nodes(true)
wenzelm@59256
    65
          val ins = degree_nodes(false)
markus@49557
    66
markus@49557
    67
          if (outs.nonEmpty || ins.nonEmpty) {
markus@49557
    68
            contents += new Separator()
wenzelm@59218
    69
            contents +=
wenzelm@59218
    70
              new Menu("Edge") {
wenzelm@59218
    71
                if (outs.nonEmpty) {
wenzelm@59247
    72
                  contents += new MenuItem("From ...") { enabled = false }
wenzelm@59256
    73
                  for ((from, tos) <- outs) {
wenzelm@59218
    74
                    contents +=
wenzelm@59247
    75
                      new Menu(quote(from.toString)) {
wenzelm@59247
    76
                        contents += new MenuItem("To ...") { enabled = false }
wenzelm@59256
    77
                        for (to <- tos) {
wenzelm@59218
    78
                          contents +=
wenzelm@59218
    79
                            new MenuItem(
wenzelm@59247
    80
                              new Action(quote(to.toString)) {
wenzelm@59218
    81
                                def apply =
wenzelm@59218
    82
                                  add_mutator(
wenzelm@59459
    83
                                    Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
wenzelm@59218
    84
                              })
wenzelm@59256
    85
                        }
wenzelm@59218
    86
                      }
wenzelm@59256
    87
                  }
wenzelm@59218
    88
                }
wenzelm@59218
    89
                if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() }
wenzelm@59218
    90
                if (ins.nonEmpty) {
wenzelm@59247
    91
                  contents += new MenuItem("To ...") { enabled = false }
wenzelm@59256
    92
                  for ((to, froms) <- ins) {
wenzelm@59218
    93
                    contents +=
wenzelm@59247
    94
                      new Menu(quote(to.toString)) {
wenzelm@59247
    95
                        contents += new MenuItem("From ...") { enabled = false }
wenzelm@59256
    96
                        for (from <- froms) {
wenzelm@59218
    97
                          contents +=
wenzelm@59218
    98
                            new MenuItem(
wenzelm@59247
    99
                              new Action(quote(from.toString)) {
wenzelm@59218
   100
                                def apply =
wenzelm@59221
   101
                                  add_mutator(
wenzelm@59459
   102
                                    Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
wenzelm@59218
   103
                              })
wenzelm@59256
   104
                        }
wenzelm@59218
   105
                      }
wenzelm@59256
   106
                  }
wenzelm@59218
   107
                }
markus@49557
   108
              }
markus@49557
   109
          }
markus@49557
   110
        }
markus@49557
   111
    }
markus@49557
   112
markus@49557
   113
    val popup = new JPopupMenu()
markus@49557
   114
wenzelm@59218
   115
    popup.add(
wenzelm@59218
   116
      new MenuItem(
wenzelm@59459
   117
        new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer)
markus@49557
   118
    popup.add(new JPopupMenu.Separator)
markus@49557
   119
wenzelm@59245
   120
    if (mouse_node.isDefined) {
wenzelm@59245
   121
      val node = mouse_node.get
wenzelm@59247
   122
      popup.add(new MenuItem("Mouse over: " + quote(node.toString)) { enabled = false }.peer)
markus@49557
   123
wenzelm@59245
   124
      popup.add(filter_context(List(node), true, "Hide", true).peer)
wenzelm@59245
   125
      popup.add(filter_context(List(node), false, "Show only", false).peer)
wenzelm@50472
   126
wenzelm@50472
   127
      popup.add(new JPopupMenu.Separator)
markus@49557
   128
    }
wenzelm@59319
   129
    if (selected_nodes.nonEmpty) {
wenzelm@59218
   130
      val text =
wenzelm@59247
   131
        if (selected_nodes.length > 1) "multiple"
wenzelm@59247
   132
        else quote(selected_nodes.head.toString)
markus@49557
   133
wenzelm@59245
   134
      popup.add(new MenuItem("Selected: " + text) { enabled = false }.peer)
markus@49557
   135
wenzelm@59245
   136
      popup.add(filter_context(selected_nodes, true, "Hide", true).peer)
wenzelm@59245
   137
      popup.add(filter_context(selected_nodes, false, "Show only", false).peer)
markus@49557
   138
      popup.add(new JPopupMenu.Separator)
markus@49557
   139
    }
markus@49557
   140
wenzelm@59408
   141
    popup.add(new MenuItem(new Action("Fit to window") {
wenzelm@59408
   142
      def apply = graph_panel.fit_to_window() }).peer
wenzelm@59408
   143
    )
wenzelm@50472
   144
markus@49557
   145
    popup
markus@49557
   146
  }
markus@49557
   147
}