--- a/src/Tools/Graphview/lib/Tools/graphview Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/lib/Tools/graphview Tue Dec 11 21:05:38 2012 +0100
@@ -16,7 +16,6 @@
"src/mutator_dialog.scala"
"src/mutator_event.scala"
"src/mutator.scala"
- "src/parameters.scala"
"src/popups.scala"
"src/shapes.scala"
"src/visualizer.scala"
--- a/src/Tools/Graphview/src/main_panel.scala Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/src/main_panel.scala Tue Dec 11 21:05:38 2012 +0100
@@ -33,8 +33,8 @@
val visualizer = new Visualizer(model)
def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
- "<html><pre style=\"font-family: " + visualizer.parameters.font_family +
- "; font-size: " + visualizer.parameters.tooltip_font_size + "px; \">" +
+ "<html><pre style=\"font-family: " + visualizer.font_family +
+ "; font-size: " + visualizer.tooltip_font_size + "px; \">" +
HTML.encode(Pretty.string_of(body)) + "</pre></html>"
val graph_panel = new Graph_Panel(visualizer, make_tooltip)
@@ -42,10 +42,9 @@
listenTo(keys)
reactions += graph_panel.reactions
- val mutator_dialog =
- new Mutator_Dialog(visualizer.parameters, model.Mutators, "Filters", "Hide", false)
+ val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)
- val color_dialog = new Mutator_Dialog(visualizer.parameters, model.Colors, "Colorations")
+ val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations")
private val chooser = new FileChooser()
chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
@@ -56,9 +55,9 @@
contents += Swing.HGlue
contents += new CheckBox(){
- selected = visualizer.parameters.arrow_heads
+ selected = visualizer.arrow_heads
action = Action("Arrow Heads"){
- visualizer.parameters.arrow_heads = selected
+ visualizer.arrow_heads = selected
graph_panel.repaint()
}
}
--- a/src/Tools/Graphview/src/mutator.scala Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/src/mutator.scala Tue Dec 11 21:05:38 2012 +0100
@@ -34,8 +34,8 @@
val Enabled = true
val Disabled = false
- def create(parameters: Parameters, m: Mutator): Mutator_Markup =
- (Mutators.Enabled, parameters.Colors.next, m)
+ 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)
--- a/src/Tools/Graphview/src/mutator_dialog.scala Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/src/mutator_dialog.scala Tue Dec 11 21:05:38 2012 +0100
@@ -19,7 +19,7 @@
class Mutator_Dialog(
- parameters: Parameters,
+ visualizer: Visualizer,
container: Mutator_Container,
caption: String,
reverse_caption: String = "Inverse",
@@ -110,7 +110,7 @@
private val addButton: Button = new Button{
action = Action("Add") {
addPanel(
- new Mutator_Panel((true, parameters.Colors.next,
+ new Mutator_Panel((true, visualizer.Colors.next,
mutatorBox.selection.item))
)
}
--- a/src/Tools/Graphview/src/parameters.scala Tue Dec 11 12:17:20 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-/* Title: Tools/Graphview/src/parameters.scala
- Author: Markus Kaiser, TU Muenchen
-
-Visual parameters.
-*/
-
-package isabelle.graphview
-
-import isabelle._
-
-import java.awt.Color
-
-
-class Parameters
-{
- val font_family: String = "IsabelleText"
- val font_size: Int = 14
- val gap_x = 20
- val pad_x = 8
- val pad_y = 5
-
- val tooltip_font_size: Int = 10
-
- var arrow_heads = false
-
- object Colors
- {
- private val Filter_Colors = List(
- new Color(0xD9, 0xF2, 0xE2), //blue
- new Color(0xFF, 0xE7, 0xD8), //orange
- new Color(0xFF, 0xFF, 0xE5), //yellow
- new Color(0xDE, 0xCE, 0xFF), //lilac
- new Color(0xCC, 0xEB, 0xFF), //turquoise
- new Color(0xFF, 0xE5, 0xE5), //red
- new Color(0xE5, 0xE5, 0xD9) //green
- )
-
- private var curr : Int = -1
- def next(): Color =
- {
- curr = (curr + 1) % Filter_Colors.length
- Filter_Colors(curr)
- }
- }
-}
--- a/src/Tools/Graphview/src/popups.scala Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/src/popups.scala Tue Dec 11 21:05:38 2012 +0100
@@ -18,10 +18,10 @@
def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String])
: JPopupMenu =
{
- val parameters = panel.visualizer.parameters
+ val visualizer = panel.visualizer
- val add_mutator = panel.visualizer.model.Mutators.add _
- val curr = panel.visualizer.model.current
+ val add_mutator = visualizer.model.Mutators.add _
+ val curr = visualizer.model.current
def filter_context(ls: List[String], reverse: Boolean,
caption: String, edges: Boolean) =
@@ -29,7 +29,7 @@
contents += new MenuItem(new Action("This") {
def apply =
add_mutator(
- Mutators.create(parameters,
+ Mutators.create(visualizer,
Node_List(ls, reverse, false, false)
)
)
@@ -38,7 +38,7 @@
contents += new MenuItem(new Action("Family") {
def apply =
add_mutator(
- Mutators.create(parameters,
+ Mutators.create(visualizer,
Node_List(ls, reverse, true, true)
)
)
@@ -47,7 +47,7 @@
contents += new MenuItem(new Action("Parents") {
def apply =
add_mutator(
- Mutators.create(parameters,
+ Mutators.create(visualizer,
Node_List(ls, reverse, false, true)
)
)
@@ -56,7 +56,7 @@
contents += new MenuItem(new Action("Children") {
def apply =
add_mutator(
- Mutators.create(parameters,
+ Mutators.create(visualizer,
Node_List(ls, reverse, true, false)
)
)
@@ -89,7 +89,7 @@
contents += new MenuItem(new Action(to) {
def apply =
add_mutator(
- Mutators.create(parameters, Edge_Endpoints(from, to))
+ Mutators.create(visualizer, Edge_Endpoints(from, to))
)
})
})
@@ -115,7 +115,7 @@
contents += new MenuItem(new Action(from) {
def apply =
add_mutator(
- Mutators.create(parameters, Edge_Endpoints(from, to))
+ Mutators.create(visualizer, Edge_Endpoints(from, to))
)
})
})
@@ -130,14 +130,14 @@
val popup = new JPopupMenu()
popup.add(new MenuItem(new Action("Remove all filters") {
- def apply = panel.visualizer.model.Mutators(Nil)
+ def apply = visualizer.model.Mutators(Nil)
}).peer
)
popup.add(new JPopupMenu.Separator)
if (under_mouse.isDefined) {
val v = under_mouse.get
- popup.add(new MenuItem("Mouseover: %s".format(panel.visualizer.Caption(v))) {
+ popup.add(new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) {
enabled = false
}.peer)
@@ -151,7 +151,7 @@
if (selected.length > 1) {
"Multiple"
} else {
- panel.visualizer.Caption(selected.head)
+ visualizer.Caption(selected.head)
}
}
--- a/src/Tools/Graphview/src/shapes.scala Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/src/shapes.scala Tue Dec 11 21:05:38 2012 +0100
@@ -28,8 +28,8 @@
{
val (x, y) = visualizer.Coordinates(peer.get)
val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g)
- val w = bounds.getWidth + visualizer.parameters.pad_x
- val h = bounds.getHeight + visualizer.parameters.pad_y
+ val w = bounds.getWidth + visualizer.pad_x
+ val h = bounds.getHeight + visualizer.pad_y
new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
}
--- a/src/Tools/Graphview/src/visualizer.scala Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala Tue Dec 11 21:05:38 2012 +0100
@@ -1,7 +1,7 @@
/* Title: Tools/Graphview/src/visualizer.scala
Author: Markus Kaiser, TU Muenchen
-Graph visualization interface.
+Graph visualization parameters and interface state.
*/
package isabelle.graphview
@@ -18,7 +18,50 @@
{
visualizer =>
- val parameters = new Parameters
+ /* font rendering information */
+
+ val font_family: String = "IsabelleText"
+ val font_size: Int = 14
+
+ val font = new Font(visualizer.font_family, Font.BOLD, visualizer.font_size)
+ val font_metrics: FontMetrics = Toolkit.getDefaultToolkit.getFontMetrics(font)
+
+ val rendering_hints =
+ new RenderingHints(
+ RenderingHints.KEY_ANTIALIASING,
+ RenderingHints.VALUE_ANTIALIAS_ON)
+
+ val tooltip_font_size: Int = 10
+
+
+ /* rendering parameters */
+
+ val gap_x = 20
+ val pad_x = 8
+ val pad_y = 5
+
+ var arrow_heads = false
+
+ object Colors
+ {
+ private val filter_colors = List(
+ new JColor(0xD9, 0xF2, 0xE2), // blue
+ new JColor(0xFF, 0xE7, 0xD8), // orange
+ new JColor(0xFF, 0xFF, 0xE5), // yellow
+ new JColor(0xDE, 0xCE, 0xFF), // lilac
+ new JColor(0xCC, 0xEB, 0xFF), // turquoise
+ new JColor(0xFF, 0xE5, 0xE5), // red
+ new JColor(0xE5, 0xE5, 0xD9) // green
+ )
+
+ private var curr : Int = -1
+ def next(): JColor =
+ {
+ curr = (curr + 1) % filter_colors.length
+ filter_colors(curr)
+ }
+ }
+
object Coordinates
{
@@ -76,10 +119,9 @@
val max_width =
model.current.entries.map({ case (_, (info, _)) =>
font_metrics.stringWidth(info.name).toDouble }).max
- val box_distance = max_width + parameters.pad_x + parameters.gap_x
+ val box_distance = max_width + visualizer.pad_x + visualizer.gap_x
def box_height(n: Int): Double =
- ((font_metrics.getAscent + font_metrics.getDescent + parameters.pad_y) * (5 max n))
- .toDouble
+ ((font_metrics.getAscent + font_metrics.getDescent + pad_y) * (5 max n)).toDouble
Layout_Pendulum(model.current, box_distance, box_height)
}
}
@@ -118,7 +160,7 @@
g.setRenderingHints(rendering_hints)
model.visible_edges().foreach(e => {
- apply(g, e, parameters.arrow_heads, dummies)
+ apply(g, e, arrow_heads, dummies)
})
model.visible_nodes().foreach(l => {
@@ -165,15 +207,4 @@
{
def apply(key: String) = model.complete.get_node(key).name
}
-
-
- /* font rendering information */
-
- val font = new Font(parameters.font_family, Font.BOLD, parameters.font_size)
- val font_metrics: FontMetrics = Toolkit.getDefaultToolkit.getFontMetrics(font)
-
- val rendering_hints =
- new RenderingHints(
- RenderingHints.KEY_ANTIALIASING,
- RenderingHints.VALUE_ANTIALIAS_ON)
}
\ No newline at end of file