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