src/Tools/Graphview/popups.scala

recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;

/*  Title:      Tools/Graphview/popups.scala
    Author:     Markus Kaiser, TU Muenchen
    Author:     Makarius

PopupMenu generation for graph components.
*/

package isabelle.graphview


import isabelle._

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_graph

    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(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, false)))
          })

        contents +=
          new MenuItem(new Action("Family") {
            def apply =
              add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, true, true)))
          })

        contents +=
          new MenuItem(new Action("Parents") {
            def apply =
              add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, true)))
          })

        contents +=
          new MenuItem(new Action("Children") {
            def apply =
              add_mutator(Mutator.make(visualizer, Mutator.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(
                                    Mutator.make(visualizer, Mutator.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(
                                    Mutator.make(visualizer, Mutator.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
  }
}