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