src/Tools/Graphview/popups.scala

+/*  Title:      Tools/Graphview/popups.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+PopupMenu generation for graph components.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+
+import javax.swing.JPopupMenu
+import scala.swing.{Action, Menu, MenuItem, Separator}
+
+
+object Popups
+{
+  def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String])
+    : JPopupMenu =
+  {
+    val visualizer = panel.visualizer
+
+    val add_mutator = visualizer.model.Mutators.add _
+    val curr = visualizer.model.current
+
+    def filter_context(ls: List[String], reverse: Boolean,
+                       caption: String, edges: Boolean) =
+      new Menu(caption) {
+        contents += new MenuItem(new Action("This") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, false, false)
+                )
+              )
+          })
+
+        contents += new MenuItem(new Action("Family") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, true, true)
+                )
+              )
+          })
+
+        contents += new MenuItem(new Action("Parents") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, false, true)
+                )
+              )
+          })
+
+        contents += new MenuItem(new Action("Children") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, true, false)
+                )
+              )
+          })
+
+
+        if (edges) {
+          val outs = ls.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
+                      .filter(_._2.size > 0).sortBy(_._1)
+          val ins = ls.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
+                      .filter(_._2.size > 0).sortBy(_._1)
+
+          if (outs.nonEmpty || ins.nonEmpty) {
+            contents += new Separator()
+
+            contents += new Menu("Edge") {
+              if (outs.nonEmpty) {
+                contents += new MenuItem("From...") {
+                  enabled = false
+                }
+
+                outs.map( e => {
+                  val (from, tos) = e
+                  contents += new Menu(from) {
+                    contents += new MenuItem("To..."){
+                      enabled = false
+                    }
+
+                    tos.toList.sorted.distinct.map( to => {
+                      contents += new MenuItem(new Action(to) {
+                        def apply =
+                          add_mutator(
+                            Mutators.create(visualizer, Edge_Endpoints(from, to))
+                          )
+                      })
+                    })
+                  }
+                })
+              }
+              if (outs.nonEmpty && ins.nonEmpty) {
+                contents += new Separator()
+              }
+              if (ins.nonEmpty) {
+                contents += new MenuItem("To...") {
+                  enabled = false
+                }
+
+                ins.map( e => {
+                  val (to, froms) = e
+                  contents += new Menu(to) {
+                    contents += new MenuItem("From..."){
+                      enabled = false
+                    }
+
+                    froms.toList.sorted.distinct.map( from => {
+                      contents += new MenuItem(new Action(from) {
+                        def apply =
+                          add_mutator(
+                            Mutators.create(visualizer, Edge_Endpoints(from, to))
+                          )
+                      })
+                    })
+                  }
+                })
+              }
+            }
+          }
+        }
+    }
+
+    val popup = new JPopupMenu()
+
+    popup.add(new MenuItem(new Action("Remove all filters") {
+          def apply = visualizer.model.Mutators(Nil)
+        }).peer
+    )
+    popup.add(new JPopupMenu.Separator)
+
+    if (under_mouse.isDefined) {
+      val v = under_mouse.get
+      popup.add(new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) {
+        enabled = false
+      }.peer)
+
+      popup.add(filter_context(List(v), true, "Hide", true).peer)
+      popup.add(filter_context(List(v), false, "Show only", false).peer)
+
+      popup.add(new JPopupMenu.Separator)
+    }
+    if (!selected.isEmpty) {
+      val text = {
+        if (selected.length > 1) {
+          "Multiple"
+        } else {
+          visualizer.Caption(selected.head)
+        }
+      }
+
+      popup.add(new MenuItem("Selected: %s".format(text)) {
+        enabled = false
+      }.peer)
+
+      popup.add(filter_context(selected, true, "Hide", true).peer)
+      popup.add(filter_context(selected, false, "Show only", false).peer)
+      popup.add(new JPopupMenu.Separator)
+    }
+
+
+    popup.add(new MenuItem(new Action("Fit to Window") {
+        def apply = panel.fit_to_window()
+      }).peer
+    )
+
+    popup
+  }
+}