--- 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,
--- 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)
}
}
}
--- 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
+}
--- 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]()
--- 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]
--- 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)))
})
})
}