Quelle popups.scala Sprache: Scala

/*  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(
    graph_panel: Graph_Panel,
    mouse_node: Option[Graph_Display.Node],
    selected_nodes: List[Graph_Display.Node]
  ): JPopupMenu = {
    val graphview = graph_panel.graphview

    val add_mutator = graphview.model.Mutators.add _
    val visible_graph = graphview.visible_graph

    def filter_context(
        nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =
      new Menu(caption) {
        contents +=
          new MenuItem(new Action("This") {
            def apply(): Unit =
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, false)))
          })

        contents +=
          new MenuItem(new Action("Family") {
            def apply(): Unit =
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, true)))
          })

        contents +=
          new MenuItem(new Action("Parents") {
            def apply(): Unit =
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, true)))
          })

        contents +=
          new MenuItem(new Action("Children") {
            def apply(): Unit =
              add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, false)))
          })

        if (edges) {
          def degree_nodes(succs: Boolean) =
            (for {
              from <- nodes.iterator
              tos = if (succs) visible_graph.imm_succs(from) else visible_graph.imm_preds(from)
              if tos.nonEmpty
            } yield (from, tos)).toList.sortBy(_._1)(Graph_Display.Node.Ordering)

          val outs = degree_nodes(true)
          val ins = degree_nodes(false)

          if (outs.nonEmpty || ins.nonEmpty) {
            contents += new Separator()
            contents +=
              new Menu("Edge") {
                if (outs.nonEmpty) {
                  contents += new MenuItem("From ...") { enabled = false }
                  for ((from, tos) <- outs) {
                    contents +=
                      new Menu(quote(from.toString)) {
                        contents += new MenuItem("To ...") { enabled = false }
                        for (to <- tos) {
                          contents +=
                            new MenuItem(
                              new Action(quote(to.toString)) {
                                def apply(): Unit =
                                  add_mutator(
                                    Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
                              })
                        }
                      }
                  }
                }
                if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() }
                if (ins.nonEmpty) {
                  contents += new MenuItem("To ...") { enabled = false }
                  for ((to, froms) <- ins) {
                    contents +=
                      new Menu(quote(to.toString)) {
                        contents += new MenuItem("From ...") { enabled = false }
                        for (from <- froms) {
                          contents +=
                            new MenuItem(
                              new Action(quote(from.toString)) {
                                def apply(): Unit =
                                  add_mutator(
                                    Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
                              })
                        }
                      }
                  }
                }
              }
          }
        }
    }

    val popup = new JPopupMenu()

    popup.add(
      new MenuItem(
        new Action("Remove all filters") { def apply(): Unit = graphview.model.Mutators(Nil) }).peer)
    popup.add(new JPopupMenu.Separator)

    if (mouse_node.isDefined) {
      val node = mouse_node.get
      popup.add(new MenuItem("Mouse over: " + quote(node.toString)) { enabled = false }.peer)

      popup.add(filter_context(List(node), true, "Hide", true).peer)
      popup.add(filter_context(List(node), false, "Show only", false).peer)

      popup.add(new JPopupMenu.Separator)
    }
    if (selected_nodes.nonEmpty) {
      val text =
        if (selected_nodes.length > 1) "multiple"
        else quote(selected_nodes.head.toString)

      popup.add(new MenuItem("Selected: " + text) { enabled = false }.peer)

      popup.add(filter_context(selected_nodes, true, "Hide", true).peer)
      popup.add(filter_context(selected_nodes, false, "Show only", false).peer)
      popup.add(new JPopupMenu.Separator)
    }

    popup.add(new MenuItem(new Action("Fit to window") {
      def apply(): Unit = graph_panel.fit_to_window() }).peer
    )

    popup
  }
}

quality90%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.