--- a/src/Tools/Graphview/src/popups.scala Tue Dec 30 11:50:34 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-/* Title: Tools/Graphview/src/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
- }
-}