# HG changeset patch # User wenzelm # Date 1420108629 -3600 # Node ID eadd82d440b04c30d2eb66b1eabf0f8ec78c25e6 # Parent ecf64bc6977813369d0e1dfee297b3e10c3ac10d tuned whitespace; diff -r ecf64bc69778 -r eadd82d440b0 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Wed Dec 31 21:45:30 2014 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Thu Jan 01 11:37:09 2015 +0100 @@ -74,19 +74,24 @@ def apply_layout() = visualizer.Coordinates.update_layout() - private class Paint_Panel extends Panel { - def set_preferred_size() { - val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() - val s = Transform.scale_discrete - val (px, py) = Transform.padding + private class Paint_Panel extends Panel + { + def set_preferred_size() + { + val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() + val s = Transform.scale_discrete + val (px, py) = Transform.padding - preferredSize = new Dimension((math.abs(maxX - minX + px) * s).toInt, - (math.abs(maxY - minY + py) * s).toInt) + preferredSize = + new Dimension( + (math.abs(maxX - minX + px) * s).toInt, + (math.abs(maxY - minY + py) * s).toInt) - revalidate() - } + revalidate() + } - override def paint(g: Graphics2D) { + override def paint(g: Graphics2D) + { super.paintComponent(g) g.transform(Transform()) @@ -102,14 +107,15 @@ listenTo(mouse.wheel) reactions += Interaction.Mouse.react reactions += Interaction.Keyboard.react - reactions += { - case KeyTyped(_, _, _, _) => {repaint(); requestFocus()} - case MousePressed(_, _, _, _, _) => {repaint(); requestFocus()} - case MouseDragged(_, _, _) => {repaint(); requestFocus()} - case MouseWheelMoved(_, _, _, _) => {repaint(); requestFocus()} - case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()} - case MouseMoved(_, _, _) => repaint() - } + reactions += + { + case KeyTyped(_, _, _, _) => repaint(); requestFocus() + case MousePressed(_, _, _, _, _) => repaint(); requestFocus() + case MouseDragged(_, _, _) => repaint(); requestFocus() + case MouseWheelMoved(_, _, _, _) => repaint(); requestFocus() + case MouseClicked(_, _, _, _, _) => repaint(); requestFocus() + case MouseMoved(_, _, _) => repaint() + } visualizer.model.Colors.events += { case _ => repaint() } visualizer.model.Mutators.events += { case _ => repaint() } @@ -130,7 +136,8 @@ def scale_discrete: Double = (_scale * visualizer.font_size).round.toDouble / visualizer.font_size - def apply() = { + def apply() = + { val (minX, minY, _, _) = visualizer.Coordinates.bounds() val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) @@ -138,7 +145,8 @@ at } - def fit_to_window() { + def fit_to_window() + { if (visualizer.model.visible_nodes_iterator.isEmpty) rescale(1.0) else { @@ -150,7 +158,8 @@ } } - def pane_to_graph_coordinates(at: Point2D): Point2D = { + def pane_to_graph_coordinates(at: Point2D): Point2D = + { val s = Transform.scale_discrete val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null) @@ -159,11 +168,14 @@ } } - object Interaction { - object Keyboard { + object Interaction + { + object Keyboard + { import scala.swing.event.Key._ - val react: PartialFunction[Event, Unit] = { + val react: PartialFunction[Event, Unit] = + { case KeyTyped(_, c, m, _) => typed(c, m) } @@ -178,28 +190,28 @@ } } - object Mouse { + object Mouse + { import scala.swing.event.Key.Modifier._ type Modifiers = Int type Dummy = ((String, String), Int) private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null - val react: PartialFunction[Event, Unit] = { + val react: PartialFunction[Event, Unit] = + { case MousePressed(_, p, _, _, _) => pressed(p) - case MouseDragged(_, to, _) => { - drag(draginfo, to) - val (_, p, d) = draginfo - draginfo = (to, p, d) - } + case MouseDragged(_, to, _) => + drag(draginfo, to) + val (_, p, d) = draginfo + draginfo = (to, p, d) case MouseWheelMoved(_, p, _, r) => wheel(r, p) - case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e) + case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e) } def dummy(at: Point2D): Option[Dummy] = - visualizer.model.visible_edges_iterator.map({ - i => visualizer.Coordinates(i).zipWithIndex.map((i, _)) - }).flatten.find({ + visualizer.model.visible_edges_iterator.map( + i => visualizer.Coordinates(i).zipWithIndex.map((i, _))).flatten.find({ case (_, ((x, y), _)) => visualizer.Drawer.shape(visualizer.gfx, None).contains(at.getX() - x, at.getY() - y) }) match { @@ -207,32 +219,35 @@ case Some((name, (_, index))) => Some((name, index)) } - def pressed(at: Point) { + def pressed(at: Point) + { val c = Transform.pane_to_graph_coordinates(at) val l = node(c) match { case Some(l) => if (visualizer.Selection(l)) visualizer.Selection() else List(l) case None => Nil } - val d = l match { - case Nil => dummy(c) match { - case Some(d) => List(d) - case None => Nil + val d = + l match { + case Nil => + dummy(c) match { + case Some(d) => List(d) + case None => Nil + } + case _ => Nil } - - case _ => Nil - } - draginfo = (at, l, d) } - def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) { + def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) + { import javax.swing.SwingUtilities val c = Transform.pane_to_graph_coordinates(at) val p = node(c) - def left_click() { + def left_click() + { (p, m) match { case (Some(l), Control) => visualizer.Selection.add(l) case (None, Control) => @@ -245,7 +260,8 @@ } } - def right_click() { + def right_click() + { val menu = Popups(panel, p, visualizer.Selection()) menu.show(panel.peer, at.x, at.y) } @@ -256,18 +272,18 @@ } } - def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) { + def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) + { val (from, p, d) = draginfo val s = Transform.scale_discrete val (dx, dy) = (to.x - from.x, to.y - from.y) (p, d) match { - case (Nil, Nil) => { + case (Nil, Nil) => val r = panel.peer.getViewport.getViewRect r.translate(-dx, -dy) paint_panel.peer.scrollRectToVisible(r) - } case (Nil, ds) => ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s))) @@ -277,7 +293,8 @@ } } - def wheel(rotation: Int, at: Point) { + def wheel(rotation: Int, at: Point) + { val at2 = Transform.pane_to_graph_coordinates(at) // > 0 -> up rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4)) @@ -287,11 +304,11 @@ val r = panel.peer.getViewport.getViewRect val (width, height) = (r.getWidth, r.getHeight) paint_panel.peer.scrollRectToVisible( - new Rectangle((at2.getX() - width / 2).toInt, - (at2.getY() - height / 2).toInt, - width.toInt, - height.toInt) - ) + new Rectangle( + (at2.getX() - width / 2).toInt, + (at2.getY() - height / 2).toInt, + width.toInt, + height.toInt)) } } } diff -r ecf64bc69778 -r eadd82d440b0 src/Tools/Graphview/model.scala --- a/src/Tools/Graphview/model.scala Wed Dec 31 21:45:30 2014 +0100 +++ b/src/Tools/Graphview/model.scala Thu Jan 01 11:37:09 2015 +0100 @@ -13,24 +13,25 @@ import java.awt.Color -class Mutator_Container(val available: List[Mutator]) { - type Mutator_Markup = (Boolean, Color, Mutator) - - val events = new Mutator_Event.Bus - - private var _mutators : List[Mutator_Markup] = Nil - def apply() = _mutators - def apply(mutators: List[Mutator_Markup]){ - _mutators = mutators - - events.event(Mutator_Event.NewList(mutators)) - } +class Mutator_Container(val available: List[Mutator]) +{ + type Mutator_Markup = (Boolean, Color, Mutator) + + val events = new Mutator_Event.Bus - def add(mutator: Mutator_Markup) = { - _mutators = _mutators ::: List(mutator) - - events.event(Mutator_Event.Add(mutator)) - } + private var _mutators : List[Mutator_Markup] = Nil + def apply() = _mutators + def apply(mutators: List[Mutator_Markup]) + { + _mutators = mutators + events.event(Mutator_Event.NewList(mutators)) + } + + def add(mutator: Mutator_Markup) + { + _mutators = _mutators ::: List(mutator) + events.event(Mutator_Event.Add(mutator)) + } } @@ -59,7 +60,8 @@ isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true) } -class Model(private val graph: Model.Graph) { +class Model(private val graph: Model.Graph) +{ val Mutators = new Mutator_Container( List( Node_Expression(".*", false, false, false), @@ -68,39 +70,39 @@ Add_Node_Expression(""), Add_Transitive_Closure(true, true) )) - + val Colors = new Mutator_Container( List( Node_Expression(".*", false, false, false), Node_List(Nil, false, false, false) - )) - + )) + def visible_nodes_iterator: Iterator[String] = current.keys_iterator - + def visible_edges_iterator: Iterator[(String, String)] = current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _))) - + def complete = graph def current: Model.Graph = - (graph /: Mutators()) { - case (g, (enabled, _, mutator)) => { - if (!enabled) g - else mutator.mutate(graph, g) - } + (graph /: Mutators()) { + case (g, (enabled, _, mutator)) => { + if (!enabled) g + else mutator.mutate(graph, g) } - + } + private var _colors = Map.empty[String, Color] def colors = _colors - - private def build_colors() { - _colors = - (Map.empty[String, Color] /: Colors()) ({ - case (colors, (enabled, color, mutator)) => { - (colors /: mutator.mutate(graph, graph).keys_iterator) ({ - case (colors, k) => colors + (k -> color) - }) - } - }) + + private def build_colors() + { + _colors = + (Map.empty[String, Color] /: Colors()) { + case (colors, (enabled, color, mutator)) => + (colors /: mutator.mutate(graph, graph).keys_iterator) { + case (colors, k) => colors + (k -> color) + } + } } Colors.events += { case _ => build_colors() } } diff -r ecf64bc69778 -r eadd82d440b0 src/Tools/Graphview/mutator.scala --- a/src/Tools/Graphview/mutator.scala Wed Dec 31 21:45:30 2014 +0100 +++ b/src/Tools/Graphview/mutator.scala Thu Jan 01 11:37:09 2015 +0100 @@ -28,120 +28,111 @@ def filter(sub: Model.Graph) : Model.Graph } -object Mutators { +object Mutators +{ type Mutator_Markup = (Boolean, Color, Mutator) - + val Enabled = true val Disabled = false - + def create(visualizer: Visualizer, m: Mutator): Mutator_Markup = (Mutators.Enabled, visualizer.Colors.next, m) - class Graph_Filter(val name: String, val description: String, - pred: Model.Graph => Model.Graph) - extends Filter + class Graph_Filter( + val name: String, + val description: String, + pred: Model.Graph => Model.Graph) extends Filter { def filter(sub: Model.Graph) : Model.Graph = pred(sub) } - class Graph_Mutator(val name: String, val description: String, - pred: (Model.Graph, Model.Graph) => Model.Graph) - extends Mutator + class Graph_Mutator( + val name: String, + val description: String, + pred: (Model.Graph, Model.Graph) => Model.Graph) extends Mutator { - def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph = - pred(complete, sub) + def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph = pred(complete, sub) } - class Node_Filter(name: String, description: String, + class Node_Filter( + name: String, + description: String, pred: (Model.Graph, String) => Boolean) - extends Graph_Filter ( - - name, - description, - g => g.restrict(pred(g, _)) - ) - - class Edge_Filter(name: String, description: String, - pred: (Model.Graph, String, String) => Boolean) - extends Graph_Filter ( + extends Graph_Filter(name, description, g => g.restrict(pred(g, _))) - name, - description, - g => (g /: g.dest) { - case (graph, ((from, _), tos)) => { - (graph /: tos) { - (gr, to) => if (pred(gr, from, to)) gr - else gr.del_edge(from, to) - } - } - } - ) + class Edge_Filter( + name: String, + description: String, + pred: (Model.Graph, String, String) => Boolean) + extends Graph_Filter( + name, + description, + g => (g /: g.dest) { + case (graph, ((from, _), tos)) => + (graph /: tos)((gr, to) => + if (pred(gr, from, to)) gr else gr.del_edge(from, to)) + }) - class Node_Family_Filter(name: String, description: String, - reverse: Boolean, parents: Boolean, children: Boolean, - pred: (Model.Graph, String) => Boolean) + class Node_Family_Filter( + name: String, + description: String, + reverse: Boolean, + parents: Boolean, + children: Boolean, + pred: (Model.Graph, String) => Boolean) extends Node_Filter( + name, + description, + (g, k) => + reverse != + (pred(g, k) || + (parents && g.all_preds(List(k)).exists(pred(g, _))) || + (children && g.all_succs(List(k)).exists(pred(g, _))))) - name, - description, - (g, k) => reverse != ( - pred(g, k) || - (parents && g.all_preds(List(k)).exists(pred(g, _))) || - (children && g.all_succs(List(k)).exists(pred(g, _))) - ) - ) - case class Identity() extends Graph_Filter( - - "Identity", - "Does not change the graph.", - g => g - ) - - case class Node_Expression(regex: String, - reverse: Boolean, parents: Boolean, children: Boolean) - extends Node_Family_Filter( + "Identity", + "Does not change the graph.", + g => g) - "Filter by Name", - "Only shows or hides all nodes with any family member's name matching " + - "a regex.", - reverse, - parents, - children, - (g, k) => (regex.r findFirstIn k).isDefined - ) + case class Node_Expression( + regex: String, + reverse: Boolean, + parents: Boolean, + children: Boolean) + extends Node_Family_Filter( + "Filter by Name", + "Only shows or hides all nodes with any family member's name matching a regex.", + reverse, + parents, + children, + (g, k) => (regex.r findFirstIn k).isDefined) - case class Node_List(list: List[String], - reverse: Boolean, parents: Boolean, children: Boolean) + case class Node_List( + list: List[String], + reverse: Boolean, + parents: Boolean, + children: Boolean) extends Node_Family_Filter( - - "Filter by Name List", - "Only shows or hides all nodes with any family member's name matching " + - "any string in a comma separated list.", - reverse, - parents, - children, - (g, k) => list.exists(_ == k) - ) + "Filter by Name List", + "Only shows or hides all nodes with any family member's name matching any string in a comma separated list.", + reverse, + parents, + children, + (g, k) => list.exists(_ == k)) case class Edge_Endpoints(source: String, dest: String) extends Edge_Filter( - - "Hide edge", - "Hides the edge whose endpoints match strings.", - (g, s, d) => !(s == source && d == dest) - ) + "Hide edge", + "Hides the edge whose endpoints match strings.", + (g, s, d) => !(s == source && d == dest)) - private def add_node_group(from: Model.Graph, to: Model.Graph, - keys: List[String]) = { - + private def add_node_group(from: Model.Graph, to: Model.Graph, keys: List[String]) = + { // Add Nodes - val with_nodes = - (to /: keys) { - (graph, key) => graph.default_node(key, from.get_node(key)) - } - + val with_nodes = + (to /: keys)((graph, key) => graph.default_node(key, from.get_node(key))) + // Add Edges (with_nodes /: keys) { (gv, key) => { @@ -156,44 +147,31 @@ } } - add_edges( add_edges(gv, from.imm_preds(key), false), - from.imm_succs(key), true - ) + from.imm_succs(key), true) } } - } - + } + case class Add_Node_Expression(regex: String) extends Graph_Mutator( + "Add by name", + "Adds every node whose name matches the regex. " + + "Adds all relevant edges.", + (complete, sub) => + add_node_group(complete, sub, + complete.keys.filter(k => (regex.r findFirstIn k).isDefined).toList)) - "Add by name", - "Adds every node whose name matches the regex. " + - "Adds all relevant edges.", - (complete, sub) => { - add_node_group(complete, sub, complete.keys.filter( - k => (regex.r findFirstIn k).isDefined - ).toList) - } - ) - case class Add_Transitive_Closure(parents: Boolean, children: Boolean) extends Graph_Mutator( - - "Add transitive closure", - "Adds all family members of all current nodes.", - (complete, sub) => { - val withparents = - if (parents) - add_node_group(complete, sub, complete.all_preds(sub.keys)) - else - sub - - if (children) - add_node_group(complete, withparents, complete.all_succs(sub.keys)) - else - withparents - } - ) + "Add transitive closure", + "Adds all family members of all current nodes.", + (complete, sub) => { + val withparents = + if (parents) add_node_group(complete, sub, complete.all_preds(sub.keys)) + else sub + if (children) add_node_group(complete, withparents, complete.all_succs(sub.keys)) + else withparents + }) } \ No newline at end of file diff -r ecf64bc69778 -r eadd82d440b0 src/Tools/Graphview/mutator_dialog.scala --- a/src/Tools/Graphview/mutator_dialog.scala Wed Dec 31 21:45:30 2014 +0100 +++ b/src/Tools/Graphview/mutator_dialog.scala Thu Jan 01 11:37:09 2015 +0100 @@ -28,25 +28,26 @@ extends Dialog { type Mutator_Markup = (Boolean, Color, Mutator) - + title = caption - + private var _panels: List[Mutator_Panel] = Nil private def panels = _panels - private def panels_= (panels: List[Mutator_Panel]) { + private def panels_=(panels: List[Mutator_Panel]) + { _panels = panels paintPanels } - container.events += { + container.events += + { case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m)) case Mutator_Event.NewList(ms) => panels = getPanels(ms) } - override def open() { - if (!visible) - panels = getPanels(container()) - + override def open() + { + if (!visible) panels = getPanels(container()) super.open } @@ -55,39 +56,46 @@ peer.setFocusTraversalPolicy(focusTraversal) private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] = - m.filter(_ match {case (_, _, Identity()) => false; case _ => true}) + m.filter(_ match { case (_, _, Identity()) => false; case _ => true }) .map(m => new Mutator_Panel(m)) - private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = + private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = panels.map(panel => panel.get_Mutator_Markup) - private def movePanelUp(m: Mutator_Panel) = { - def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { - case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs) - case _ => l - } + private def movePanelUp(m: Mutator_Panel) = + { + def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = + l match { + case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs) + case _ => l + } panels = moveUp(panels) } - private def movePanelDown(m: Mutator_Panel) = { - def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { - case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs) - case _ => l - } + private def movePanelDown(m: Mutator_Panel) = + { + def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = + l match { + case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs) + case _ => l + } panels = moveDown(panels) } - private def removePanel(m: Mutator_Panel) = { + private def removePanel(m: Mutator_Panel) + { panels = panels.filter(_ != m).toList } - private def addPanel(m: Mutator_Panel) = { + private def addPanel(m: Mutator_Panel) + { panels = panels ::: List(m) } - def paintPanels = { + def paintPanels + { focusTraversal.clear filterPanel.contents.clear panels.map(x => { @@ -108,16 +116,13 @@ private val mutatorBox = new ComboBox[Mutator](container.available) - private val addButton: Button = new Button{ + private val addButton: Button = new Button { action = Action("Add") { - addPanel( - new Mutator_Panel((true, visualizer.Colors.next, - mutatorBox.selection.item)) - ) + addPanel(new Mutator_Panel((true, visualizer.Colors.next, mutatorBox.selection.item))) } } - private val applyButton = new Button{ + private val applyButton = new Button { action = Action("Apply") { container(getMutators(panels)) } @@ -129,11 +134,11 @@ } } - private val cancelButton = new Button{ - action = Action("Close") { - close - } + private val cancelButton = new Button { + action = Action("Close") { + close } + } defaultButton = cancelButton private val botPanel = new BoxPanel(Orientation.Horizontal) { @@ -153,7 +158,7 @@ contents += Swing.RigidBox(new Dimension(5, 0)) contents += cancelButton } - + contents = new BorderPanel { border = new EmptyBorder(5, 5, 5, 5) @@ -165,7 +170,7 @@ extends BoxPanel(Orientation.Horizontal) { private val (_enabled, _color, _mutator) = initials - + private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs() var focusList = List.empty[java.awt.Component] private val enabledBox = new iCheckBox("Enabled", _enabled) @@ -183,17 +188,16 @@ contents += enabledBox contents += Swing.RigidBox(new Dimension(5, 0)) focusList = enabledBox.peer :: focusList - inputs.map( _ match { - case (n, c) => { - contents += Swing.RigidBox(new Dimension(10, 0)) + inputs.map(_ match { + case (n, c) => + contents += Swing.RigidBox(new Dimension(10, 0)) if (n != "") { contents += new Label(n) contents += Swing.RigidBox(new Dimension(5, 0)) } contents += c.asInstanceOf[Component] - + focusList = c.asInstanceOf[Component].peer :: focusList - } case _ => }) @@ -249,23 +253,22 @@ focusList = focusList.reverse - private def isRegex(regex: String): Boolean = { - try { - regex.r + private def isRegex(regex: String): Boolean = + { + try { regex.r; true } + catch { case _: java.util.regex.PatternSyntaxException => false } + } - true - } catch { - case _: java.util.regex.PatternSyntaxException => false - } - } - - def get_Mutator_Markup: Mutator_Markup = { - def regexOrElse(regex: String, orElse: String): String = { + def get_Mutator_Markup: Mutator_Markup = + { + def regexOrElse(regex: String, orElse: String): String = + { if (isRegex(regex)) regex else orElse } - - val m = _mutator match { + + val m = _mutator match + { case Identity() => Identity() case Node_Expression(r, _, _, _) => @@ -274,68 +277,57 @@ inputs(3)._2.getBool, // "Parents" means "Show parents" or "Matching Children" inputs(1)._2.getBool, - inputs(0)._2.getBool - ) + inputs(0)._2.getBool) case Node_List(_, _, _, _) => Node_List( inputs(2)._2.getString.split(',').filter(_ != "").toList, inputs(3)._2.getBool, // "Parents" means "Show parents" or "Matching Children" inputs(1)._2.getBool, - inputs(0)._2.getBool - ) + inputs(0)._2.getBool) case Edge_Endpoints(_, _) => Edge_Endpoints( inputs(0)._2.getString, - inputs(1)._2.getString - ) + inputs(1)._2.getString) case Add_Node_Expression(r) => - Add_Node_Expression( - regexOrElse(inputs(0)._2.getString, r) - ) + Add_Node_Expression(regexOrElse(inputs(0)._2.getString, r)) case Add_Transitive_Closure(_, _) => Add_Transitive_Closure( inputs(0)._2.getBool, - inputs(1)._2.getBool - ) + inputs(1)._2.getBool) case _ => Identity() } - + (enabledBox.selected, background, m) } - - private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match { - case Node_Expression(regex, reverse, check_parents, check_children) => - List( - ("", new iCheckBox("Parents", check_children)), - ("", new iCheckBox("Children", check_parents)), - ("Regex", new iTextField(regex, x => !isRegex(x))), - ("", new iCheckBox(reverse_caption, reverse)) - ) - case Node_List(list, reverse, check_parents, check_children) => - List( - ("", new iCheckBox("Parents", check_children)), - ("", new iCheckBox("Children", check_parents)), - ("Names", new iTextField(list.mkString(","))), - ("", new iCheckBox(reverse_caption, reverse)) - ) - case Edge_Endpoints(source, dest) => - List( - ("Source", new iTextField(source)), - ("Destination", new iTextField(dest)) - ) - case Add_Node_Expression(regex) => - List( - ("Regex", new iTextField(regex, x => !isRegex(x))) - ) - case Add_Transitive_Closure(parents, children) => - List( - ("", new iCheckBox("Parents", parents)), - ("", new iCheckBox("Children", children)) - ) - case _ => Nil - } + + private def get_Inputs(): List[(String, Mutator_Input_Value)] = + _mutator match { + case Node_Expression(regex, reverse, check_parents, check_children) => + List( + ("", new iCheckBox("Parents", check_children)), + ("", new iCheckBox("Children", check_parents)), + ("Regex", new iTextField(regex, x => !isRegex(x))), + ("", new iCheckBox(reverse_caption, reverse))) + case Node_List(list, reverse, check_parents, check_children) => + List( + ("", new iCheckBox("Parents", check_children)), + ("", new iCheckBox("Children", check_parents)), + ("Names", new iTextField(list.mkString(","))), + ("", new iCheckBox(reverse_caption, reverse))) + case Edge_Endpoints(source, dest) => + List( + ("Source", new iTextField(source)), + ("Destination", new iTextField(dest))) + case Add_Node_Expression(regex) => + List(("Regex", new iTextField(regex, x => !isRegex(x)))) + case Add_Transitive_Closure(parents, children) => + List( + ("", new iCheckBox("Parents", parents)), + ("", new iCheckBox("Children", children))) + case _ => Nil + } } private trait Mutator_Input_Value @@ -351,12 +343,11 @@ preferredSize = new Dimension(125, 18) - reactions += { + reactions += + { case ValueChanged(_) => - if (colorator(text)) - background = Color.RED - else - background = Color.WHITE + if (colorator(text)) background = Color.RED + else background = Color.WHITE } def getString = text @@ -372,56 +363,35 @@ def getBool = selected } - private object focusTraversal - extends FocusTraversalPolicy + private object focusTraversal extends FocusTraversalPolicy { private var items = Vector[java.awt.Component]() - def add(c: java.awt.Component) { - items = items :+ c - } - def addAll(cs: TraversableOnce[java.awt.Component]) { - items = items ++ cs - } - def clear() { - items = Vector[java.awt.Component]() - } + def add(c: java.awt.Component) { items = items :+ c } + def addAll(cs: TraversableOnce[java.awt.Component]) { items = items ++ cs } + def clear() { items = Vector[java.awt.Component]() } - def getComponentAfter(root: java.awt.Container, - c: java.awt.Component): java.awt.Component = { + def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component = + { val i = items.indexOf(c) - if (i < 0) { - getDefaultComponent(root) - } else { - items((i + 1) % items.length) - } + if (i < 0) getDefaultComponent(root) + else items((i + 1) % items.length) } - def getComponentBefore(root: java.awt.Container, - c: java.awt.Component): java.awt.Component = { + def getComponentBefore(root: java.awt.Container, c: java.awt.Component): java.awt.Component = + { val i = items.indexOf(c) - if (i < 0) { - getDefaultComponent(root) - } else { - items((i - 1) % items.length) - } + if (i < 0) getDefaultComponent(root) + else items((i - 1) % items.length) } - def getFirstComponent(root: java.awt.Container): java.awt.Component = { - if (items.length > 0) - items(0) - else - null - } + def getFirstComponent(root: java.awt.Container): java.awt.Component = + if (items.length > 0) items(0) else null - def getDefaultComponent(root: java.awt.Container) - : java.awt.Component = getFirstComponent(root) + def getDefaultComponent(root: java.awt.Container): java.awt.Component = + getFirstComponent(root) - def getLastComponent(root: java.awt.Container): java.awt.Component = { - if (items.length > 0) - items.last - else - null - } + def getLastComponent(root: java.awt.Container): java.awt.Component = + if (items.length > 0) items.last else null } } \ No newline at end of file diff -r ecf64bc69778 -r eadd82d440b0 src/Tools/Graphview/popups.scala --- a/src/Tools/Graphview/popups.scala Wed Dec 31 21:45:30 2014 +0100 +++ b/src/Tools/Graphview/popups.scala Thu Jan 01 11:37:09 2015 +0100 @@ -16,131 +16,113 @@ object Popups { - def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String]) - : JPopupMenu = + 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) = + def filter_context(ls: List[String], reverse: Boolean, caption: String, edges: Boolean) = new Menu(caption) { - contents += new MenuItem(new Action("This") { + contents += + new MenuItem(new Action("This") { def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, false, false) - ) - ) + add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, false, false))) }) - contents += new MenuItem(new Action("Family") { + contents += + new MenuItem(new Action("Family") { def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, true, true) - ) - ) + add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, true, true))) }) - contents += new MenuItem(new Action("Parents") { + contents += + new MenuItem(new Action("Parents") { def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, false, true) - ) - ) + add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, false, true))) }) - contents += new MenuItem(new Action("Children") { + contents += + new MenuItem(new Action("Children") { def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, true, false) - ) - ) + 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) + 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 - } + 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 - } + 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 } - tos.toList.sorted.distinct.map( to => { - contents += new MenuItem(new Action(to) { - def apply = - add_mutator( - Mutators.create(visualizer, Edge_Endpoints(from, to)) - ) - }) - }) - } - }) + 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))) + }) + }) + } + }) + } } - 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") { + popup.add( + new MenuItem( + new Action("Remove all filters") { def apply = visualizer.model.Mutators(Nil) - }).peer - ) + }).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( + 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) @@ -148,28 +130,19 @@ popup.add(new JPopupMenu.Separator) } if (!selected.isEmpty) { - val text = { - if (selected.length > 1) { - "Multiple" - } else { - visualizer.Caption(selected.head) - } - } + 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(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.add( + new MenuItem(new Action("Fit to Window") { def apply = panel.fit_to_window() }).peer) popup }