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