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;
     1 /*  Title:      Tools/Graphview/popups.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 PopupMenu generation for graph components.
     6 */
     7 
     8 package isabelle.graphview
     9 
    10 
    11 import isabelle._
    12 
    13 import javax.swing.JPopupMenu
    14 import scala.swing.{Action, Menu, MenuItem, Separator}
    15 
    16 
    17 object 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 }