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