--- 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))
}
}
}
--- 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() }
}
--- 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
--- 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
--- 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
}