# HG changeset patch # User wenzelm # Date 1420114050 -3600 # Node ID f779f83ef4ecc5b49f0a4fa0a9b9fc12fab4f78a # Parent 261ec482cd406494eb3d6872d7a76d42bce0a57b tuned signature; diff -r 261ec482cd40 -r f779f83ef4ec src/Tools/Graphview/main_panel.scala --- a/src/Tools/Graphview/main_panel.scala Thu Jan 01 12:34:15 2015 +0100 +++ b/src/Tools/Graphview/main_panel.scala Thu Jan 01 13:07:30 2015 +0100 @@ -8,7 +8,6 @@ import isabelle._ -import isabelle.graphview.Mutators._ import scala.collection.JavaConversions._ import scala.swing.{BorderPanel, Button, BoxPanel, diff -r 261ec482cd40 -r f779f83ef4ec src/Tools/Graphview/model.scala --- a/src/Tools/Graphview/model.scala Thu Jan 01 12:34:15 2015 +0100 +++ b/src/Tools/Graphview/model.scala Thu Jan 01 13:07:30 2015 +0100 @@ -8,26 +8,23 @@ import isabelle._ -import isabelle.graphview.Mutators._ 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 + private var _mutators : List[Mutator.Info] = Nil def apply() = _mutators - def apply(mutators: List[Mutator_Markup]) + def apply(mutators: List[Mutator.Info]) { _mutators = mutators - events.event(Mutator_Event.NewList(mutators)) + events.event(Mutator_Event.New_List(mutators)) } - def add(mutator: Mutator_Markup) + def add(mutator: Mutator.Info) { _mutators = _mutators ::: List(mutator) events.event(Mutator_Event.Add(mutator)) @@ -62,20 +59,20 @@ class Model(private val graph: Model.Graph) { - val Mutators = new Mutator_Container( - List( - Node_Expression(".*", false, false, false), - Node_List(Nil, false, false, false), - Edge_Endpoints("", ""), - Add_Node_Expression(""), - Add_Transitive_Closure(true, true) - )) + val Mutators = + new Mutator_Container( + List( + Mutator.Node_Expression(".*", false, false, false), + Mutator.Node_List(Nil, false, false, false), + Mutator.Edge_Endpoints("", ""), + Mutator.Add_Node_Expression(""), + Mutator.Add_Transitive_Closure(true, true))) - val Colors = new Mutator_Container( - List( - Node_Expression(".*", false, false, false), - Node_List(Nil, false, false, false) - )) + val Colors = + new Mutator_Container( + List( + Mutator.Node_Expression(".*", false, false, false), + Mutator.Node_List(Nil, false, false, false))) def visible_nodes_iterator: Iterator[String] = current.keys_iterator @@ -85,10 +82,7 @@ def complete = graph def current: Model.Graph = (graph /: Mutators()) { - case (g, (enabled, _, mutator)) => { - if (!enabled) g - else mutator.mutate(graph, g) - } + case (g, m) => if (!m.enabled) g else m.mutator.mutate(graph, g) } private var _colors = Map.empty[String, Color] @@ -98,9 +92,9 @@ { _colors = (Map.empty[String, Color] /: Colors()) { - case (colors, (enabled, color, mutator)) => - (colors /: mutator.mutate(graph, graph).keys_iterator) { - case (colors, k) => colors + (k -> color) + case (colors, m) => + (colors /: m.mutator.mutate(graph, graph).keys_iterator) { + case (colors, k) => colors + (k -> m.color) } } } diff -r 261ec482cd40 -r f779f83ef4ec src/Tools/Graphview/mutator.scala --- a/src/Tools/Graphview/mutator.scala Thu Jan 01 12:34:15 2015 +0100 +++ b/src/Tools/Graphview/mutator.scala Thu Jan 01 13:07:30 2015 +0100 @@ -13,30 +13,12 @@ import scala.collection.immutable.SortedSet -trait Mutator -{ - val name: String - val description: String - def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph - - override def toString: String = name -} - -trait Filter extends Mutator +object Mutator { - def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub) - def filter(sub: Model.Graph) : Model.Graph -} + sealed case class Info(enabled: Boolean, color: Color, mutator: Mutator) -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) + def make(visualizer: Visualizer, m: Mutator): Info = + Info(true, visualizer.Colors.next, m) class Graph_Filter( val name: String, @@ -174,4 +156,19 @@ if (children) add_node_group(complete, withparents, complete.all_succs(sub.keys)) else withparents }) -} \ No newline at end of file +} + +trait Mutator +{ + val name: String + val description: String + def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph + + override def toString: String = name +} + +trait Filter extends Mutator +{ + def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub) + def filter(sub: Model.Graph) : Model.Graph +} diff -r 261ec482cd40 -r f779f83ef4ec src/Tools/Graphview/mutator_dialog.scala --- a/src/Tools/Graphview/mutator_dialog.scala Thu Jan 01 12:34:15 2015 +0100 +++ b/src/Tools/Graphview/mutator_dialog.scala Thu Jan 01 13:07:30 2015 +0100 @@ -15,7 +15,6 @@ import javax.swing.border.EmptyBorder import scala.collection.JavaConversions._ import scala.swing._ -import isabelle.graphview.Mutators._ import scala.swing.event.ValueChanged @@ -27,8 +26,6 @@ show_color_chooser: Boolean = true) extends Dialog { - type Mutator_Markup = (Boolean, Color, Mutator) - title = caption private var _panels: List[Mutator_Panel] = Nil @@ -42,25 +39,25 @@ container.events += { case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m)) - case Mutator_Event.NewList(ms) => panels = getPanels(ms) + case Mutator_Event.New_List(ms) => panels = get_panels(ms) } override def open() { - if (!visible) panels = getPanels(container()) + if (!visible) panels = get_panels(container()) super.open } minimumSize = new Dimension(700, 200) preferredSize = new Dimension(1000, 300) - peer.setFocusTraversalPolicy(focusTraversal) + peer.setFocusTraversalPolicy(Focus_Traversal) - private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] = - m.filter(_ match { case (_, _, Identity()) => false; case _ => true }) + private def get_panels(m: List[Mutator.Info]): List[Mutator_Panel] = + m.filter({ case Mutator.Info(_, _, Mutator.Identity()) => false case _ => true }) .map(m => new Mutator_Panel(m)) - private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = - panels.map(panel => panel.get_Mutator_Markup) + private def get_mutators(panels: List[Mutator_Panel]): List[Mutator.Info] = + panels.map(panel => panel.get_mutator) private def movePanelUp(m: Mutator_Panel) = { @@ -96,67 +93,62 @@ def paintPanels { - focusTraversal.clear + Focus_Traversal.clear filterPanel.contents.clear panels.map(x => { filterPanel.contents += x - focusTraversal.addAll(x.focusList) + Focus_Traversal.addAll(x.focusList) }) filterPanel.contents += Swing.VGlue - focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component]) - focusTraversal.add(addButton.peer) - focusTraversal.add(applyButton.peer) - focusTraversal.add(cancelButton.peer) + Focus_Traversal.add(mutator_box.peer.asInstanceOf[java.awt.Component]) + Focus_Traversal.add(add_button.peer) + Focus_Traversal.add(apply_button.peer) + Focus_Traversal.add(cancel_button.peer) filterPanel.revalidate filterPanel.repaint } val filterPanel = new BoxPanel(Orientation.Vertical) {} - private val mutatorBox = new ComboBox[Mutator](container.available) + private val mutator_box = new ComboBox[Mutator](container.available) - private val addButton: Button = new Button { + private val add_button: Button = new Button { action = Action("Add") { - addPanel(new Mutator_Panel((true, visualizer.Colors.next, mutatorBox.selection.item))) + addPanel( + new Mutator_Panel(Mutator.Info(true, visualizer.Colors.next, mutator_box.selection.item))) } } - private val applyButton = new Button { - action = Action("Apply") { - container(getMutators(panels)) - } + private val apply_button = new Button { + action = Action("Apply") { container(get_mutators(panels)) } } - private val resetButton = new Button { - action = Action("Reset") { - panels = getPanels(container()) - } + private val reset_button = new Button { + action = Action("Reset") { panels = get_panels(container()) } } - private val cancelButton = new Button { - action = Action("Close") { - close - } + private val cancel_button = new Button { + action = Action("Close") { close } } - defaultButton = cancelButton + defaultButton = cancel_button private val botPanel = new BoxPanel(Orientation.Horizontal) { border = new EmptyBorder(10, 0, 0, 0) - contents += mutatorBox + contents += mutator_box contents += Swing.RigidBox(new Dimension(10, 0)) - contents += addButton + contents += add_button contents += Swing.HGlue contents += Swing.RigidBox(new Dimension(30, 0)) - contents += applyButton + contents += apply_button contents += Swing.RigidBox(new Dimension(5, 0)) - contents += resetButton + contents += reset_button contents += Swing.RigidBox(new Dimension(5, 0)) - contents += cancelButton + contents += cancel_button } contents = new BorderPanel { @@ -166,23 +158,21 @@ add(botPanel, BorderPanel.Position.South) } - private class Mutator_Panel(initials: Mutator_Markup) + private class Mutator_Panel(initials: Mutator.Info) 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) + private val enabledBox = new iCheckBox("Enabled", initials.enabled) border = new EmptyBorder(5, 5, 5, 5) maximumSize = new Dimension(Integer.MAX_VALUE, 30) - background = _color + background = initials.color - contents += new Label(_mutator.name) { + contents += new Label(initials.mutator.name) { preferredSize = new Dimension(175, 20) horizontalAlignment = Alignment.Left - if (_mutator.description != "") tooltip = _mutator.description + if (initials.mutator.description != "") tooltip = initials.mutator.description } contents += Swing.RigidBox(new Dimension(10, 0)) contents += enabledBox @@ -259,7 +249,7 @@ catch { case _: java.util.regex.PatternSyntaxException => false } } - def get_Mutator_Markup: Mutator_Markup = + def get_mutator: Mutator.Info = { def regexOrElse(regex: String, orElse: String): String = { @@ -267,62 +257,62 @@ else orElse } - val m = _mutator match - { - case Identity() => - Identity() - case Node_Expression(r, _, _, _) => - Node_Expression( - regexOrElse(inputs(2)._2.getString, r), - inputs(3)._2.getBool, - // "Parents" means "Show parents" or "Matching Children" - inputs(1)._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) - case Edge_Endpoints(_, _) => - Edge_Endpoints( - inputs(0)._2.getString, - inputs(1)._2.getString) - case Add_Node_Expression(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) - case _ => - Identity() - } + val m = + initials.mutator match { + case Mutator.Identity() => + Mutator.Identity() + case Mutator.Node_Expression(r, _, _, _) => + Mutator.Node_Expression( + regexOrElse(inputs(2)._2.getString, r), + inputs(3)._2.getBool, + // "Parents" means "Show parents" or "Matching Children" + inputs(1)._2.getBool, + inputs(0)._2.getBool) + case Mutator.Node_List(_, _, _, _) => + Mutator.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) + case Mutator.Edge_Endpoints(_, _) => + Mutator.Edge_Endpoints( + inputs(0)._2.getString, + inputs(1)._2.getString) + case Mutator.Add_Node_Expression(r) => + Mutator.Add_Node_Expression(regexOrElse(inputs(0)._2.getString, r)) + case Mutator.Add_Transitive_Closure(_, _) => + Mutator.Add_Transitive_Closure( + inputs(0)._2.getBool, + inputs(1)._2.getBool) + case _ => + Mutator.Identity() + } - (enabledBox.selected, background, m) + Mutator.Info(enabledBox.selected, background, m) } private def get_Inputs(): List[(String, Mutator_Input_Value)] = - _mutator match { - case Node_Expression(regex, reverse, check_parents, check_children) => + initials.mutator match { + case Mutator.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) => + case Mutator.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) => + case Mutator.Edge_Endpoints(source, dest) => List( ("Source", new iTextField(source)), ("Destination", new iTextField(dest))) - case Add_Node_Expression(regex) => + case Mutator.Add_Node_Expression(regex) => List(("Regex", new iTextField(regex, x => !isRegex(x)))) - case Add_Transitive_Closure(parents, children) => + case Mutator.Add_Transitive_Closure(parents, children) => List( ("", new iCheckBox("Parents", parents)), ("", new iCheckBox("Children", children))) @@ -363,7 +353,7 @@ def getBool = selected } - private object focusTraversal extends FocusTraversalPolicy + private object Focus_Traversal extends FocusTraversalPolicy { private var items = Vector[java.awt.Component]() diff -r 261ec482cd40 -r f779f83ef4ec src/Tools/Graphview/mutator_event.scala --- a/src/Tools/Graphview/mutator_event.scala Thu Jan 01 12:34:15 2015 +0100 +++ b/src/Tools/Graphview/mutator_event.scala Thu Jan 01 13:07:30 2015 +0100 @@ -16,11 +16,9 @@ object Mutator_Event { - type Mutator_Markup = (Boolean, Color, Mutator) - sealed abstract class Message - case class Add(m: Mutator_Markup) extends Message - case class NewList(m: List[Mutator_Markup]) extends Message + case class Add(m: Mutator.Info) extends Message + case class New_List(m: List[Mutator.Info]) extends Message type Receiver = PartialFunction[Message, Unit] diff -r 261ec482cd40 -r f779f83ef4ec src/Tools/Graphview/popups.scala --- a/src/Tools/Graphview/popups.scala Thu Jan 01 12:34:15 2015 +0100 +++ b/src/Tools/Graphview/popups.scala Thu Jan 01 13:07:30 2015 +0100 @@ -8,7 +8,6 @@ import isabelle._ -import isabelle.graphview.Mutators._ import javax.swing.JPopupMenu import scala.swing.{Action, Menu, MenuItem, Separator} @@ -28,25 +27,25 @@ contents += new MenuItem(new Action("This") { def apply = - add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, false, false))) + add_mutator(Mutator.make(visualizer, Mutator.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))) + add_mutator(Mutator.make(visualizer, Mutator.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))) + add_mutator(Mutator.make(visualizer, Mutator.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))) + add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, true, false))) }) if (edges) { @@ -70,15 +69,14 @@ 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)) - ) + Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to))) }) }) } @@ -93,13 +91,14 @@ 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))) + add_mutator( + Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to))) }) }) }