separate instance of class Parameters for each Main_Panel -- avoid global program state;
misc tuning;
--- a/src/Tools/Graphview/src/main_panel.scala Mon Dec 10 21:28:01 2012 +0100
+++ b/src/Tools/Graphview/src/main_panel.scala Mon Dec 10 21:55:57 2012 +0100
@@ -26,45 +26,39 @@
class Main_Panel(graph: Model.Graph)
extends BorderPanel
{
+ focusable = true
+ requestFocus()
+
+ val model = new Model(graph)
+ val visualizer = new Visualizer(model)
+
def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
- "<html><pre style=\"font-family: " + Parameters.font_family +
- "; font-size: " + Parameters.tooltip_font_size + "px; \">" +
+ "<html><pre style=\"font-family: " + visualizer.parameters.font_family +
+ "; font-size: " + visualizer.parameters.tooltip_font_size + "px; \">" +
HTML.encode(Pretty.string_of(body)) + "</pre></html>"
- focusable = true
- requestFocus()
-
- val model = new Model(graph)
- val visualizer = new Visualizer(model)
val graph_panel = new Graph_Panel(visualizer, make_tooltip)
-
+
listenTo(keys)
reactions += graph_panel.reactions
- val mutator_dialog = new Mutator_Dialog(
- model.Mutators,
- "Filters",
- "Hide",
- false
- )
+ val mutator_dialog =
+ new Mutator_Dialog(visualizer.parameters, model.Mutators, "Filters", "Hide", false)
- val color_dialog = new Mutator_Dialog(
- model.Colors,
- "Colorations"
- )
+ val color_dialog = new Mutator_Dialog(visualizer.parameters, model.Colors, "Colorations")
private val chooser = new FileChooser()
chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
chooser.title = "Graph export"
-
+
val options_panel = new BoxPanel(Orientation.Horizontal) {
border = new EmptyBorder(0, 0, 10, 0)
contents += Swing.HGlue
contents += new CheckBox(){
- selected = Parameters.arrow_heads
+ selected = visualizer.parameters.arrow_heads
action = Action("Arrow Heads"){
- Parameters.arrow_heads = selected
+ visualizer.parameters.arrow_heads = selected
graph_panel.repaint()
}
}
@@ -72,26 +66,23 @@
contents += new Button{
action = Action("Save as PNG"){
chooser.showSaveDialog(this) match {
- case FileChooser.Result.Approve => {
- export(chooser.selectedFile)
- }
-
+ case FileChooser.Result.Approve => export(chooser.selectedFile)
case _ =>
}
}
- }
+ }
contents += Swing.RigidBox(new Dimension(10, 0))
contents += new Button{
action = Action("Apply Layout"){
graph_panel.apply_layout()
}
- }
+ }
contents += Swing.RigidBox(new Dimension(10, 0))
contents += new Button{
action = Action("Fit to Window"){
graph_panel.fit_to_window()
}
- }
+ }
contents += Swing.RigidBox(new Dimension(10, 0))
contents += new Button{
action = Action("Colorations"){
@@ -108,7 +99,7 @@
add(graph_panel, BorderPanel.Position.Center)
add(options_panel, BorderPanel.Position.North)
-
+
private def export(file: File) {
val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
@@ -120,8 +111,8 @@
g.translate(- minX + 200, - minY + 100)
visualizer.Drawer.paint_all_visible(g, false)
- g.dispose()
-
+ g.dispose()
+
try { ImageIO.write(img, "png", file) }
catch { case ex: Exception => ex.printStackTrace } // FIXME !?
}
--- a/src/Tools/Graphview/src/mutator.scala Mon Dec 10 21:28:01 2012 +0100
+++ b/src/Tools/Graphview/src/mutator.scala Mon Dec 10 21:55:57 2012 +0100
@@ -34,8 +34,8 @@
val Enabled = true
val Disabled = false
- def create(m: Mutator): Mutator_Markup =
- (Mutators.Enabled, Parameters.Colors.next, m)
+ def create(parameters: Parameters, m: Mutator): Mutator_Markup =
+ (Mutators.Enabled, parameters.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 Mon Dec 10 21:28:01 2012 +0100
+++ b/src/Tools/Graphview/src/mutator_dialog.scala Mon Dec 10 21:55:57 2012 +0100
@@ -19,7 +19,9 @@
class Mutator_Dialog(
- container: Mutator_Container, caption: String,
+ parameters: Parameters,
+ container: Mutator_Container,
+ caption: String,
reverse_caption: String = "Inverse",
show_color_chooser: Boolean = true)
extends Dialog
@@ -108,7 +110,7 @@
private val addButton: Button = new Button{
action = Action("Add") {
addPanel(
- new Mutator_Panel((true, Parameters.Colors.next,
+ new Mutator_Panel((true, parameters.Colors.next,
mutatorBox.selection.item))
)
}
@@ -159,7 +161,7 @@
}
private class Mutator_Panel(initials: Mutator_Markup)
- extends BoxPanel(Orientation.Horizontal)
+ extends BoxPanel(Orientation.Horizontal)
{
private val (_enabled, _color, _mutator) = initials
@@ -370,7 +372,7 @@
}
private object focusTraversal
- extends FocusTraversalPolicy
+ extends FocusTraversalPolicy
{
private var items = Vector[java.awt.Component]()
--- a/src/Tools/Graphview/src/parameters.scala Mon Dec 10 21:28:01 2012 +0100
+++ b/src/Tools/Graphview/src/parameters.scala Mon Dec 10 21:55:57 2012 +0100
@@ -1,7 +1,7 @@
/* Title: Tools/Graphview/src/parameters.scala
Author: Markus Kaiser, TU Muenchen
-Visual parameters with fallbacks for non-jEdit-environment.
+Visual parameters.
*/
package isabelle.graphview
@@ -11,16 +11,17 @@
import java.awt.Color
-object Parameters
+class Parameters
{
val font_family: String = "IsabelleText"
val font_size: Int = 16
val tooltip_font_size: Int = 10
+ var arrow_heads = false
- object Colors {
- val Filter_Colors = List(
-
+ 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
@@ -31,16 +32,10 @@
)
private var curr : Int = -1
- def next = {
- this.synchronized {
- curr = (curr + 1) % Filter_Colors.length
- Filter_Colors(curr)
- }
+ def next(): Color =
+ {
+ curr = (curr + 1) % Filter_Colors.length
+ Filter_Colors(curr)
}
-
- val Default = Color.WHITE
- val No_Axioms = Color.LIGHT_GRAY
}
-
- var arrow_heads = false
}
--- a/src/Tools/Graphview/src/popups.scala Mon Dec 10 21:28:01 2012 +0100
+++ b/src/Tools/Graphview/src/popups.scala Mon Dec 10 21:55:57 2012 +0100
@@ -13,20 +13,23 @@
import scala.swing.{Action, Menu, MenuItem, Separator}
-object Popups {
- def apply(panel: Graph_Panel, under_mouse: Option[String],
- selected: List[String]): JPopupMenu =
+object Popups
+{
+ def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String])
+ : JPopupMenu =
{
+ val parameters = panel.visualizer.parameters
+
val add_mutator = panel.visualizer.model.Mutators.add _
val curr = panel.visualizer.model.current
-
+
def filter_context(ls: List[String], reverse: Boolean,
caption: String, edges: Boolean) =
new Menu(caption) {
contents += new MenuItem(new Action("This") {
def apply =
add_mutator(
- Mutators.create(
+ Mutators.create(parameters,
Node_List(ls, reverse, false, false)
)
)
@@ -35,7 +38,7 @@
contents += new MenuItem(new Action("Family") {
def apply =
add_mutator(
- Mutators.create(
+ Mutators.create(parameters,
Node_List(ls, reverse, true, true)
)
)
@@ -44,7 +47,7 @@
contents += new MenuItem(new Action("Parents") {
def apply =
add_mutator(
- Mutators.create(
+ Mutators.create(parameters,
Node_List(ls, reverse, false, true)
)
)
@@ -53,7 +56,7 @@
contents += new MenuItem(new Action("Children") {
def apply =
add_mutator(
- Mutators.create(
+ Mutators.create(parameters,
Node_List(ls, reverse, true, false)
)
)
@@ -86,7 +89,7 @@
contents += new MenuItem(new Action(to) {
def apply =
add_mutator(
- Mutators.create(Edge_Endpoints(from, to))
+ Mutators.create(parameters, Edge_Endpoints(from, to))
)
})
})
@@ -94,7 +97,7 @@
})
}
if (outs.nonEmpty && ins.nonEmpty) {
- contents += new Separator()
+ contents += new Separator()
}
if (ins.nonEmpty) {
contents += new MenuItem("To...") {
@@ -112,13 +115,13 @@
contents += new MenuItem(new Action(from) {
def apply =
add_mutator(
- Mutators.create(Edge_Endpoints(from, to))
+ Mutators.create(parameters, Edge_Endpoints(from, to))
)
})
})
}
})
- }
+ }
}
}
}
@@ -140,8 +143,8 @@
popup.add(filter_context(List(v), true, "Hide", true).peer)
popup.add(filter_context(List(v), false, "Show only", false).peer)
-
- popup.add(new JPopupMenu.Separator)
+
+ popup.add(new JPopupMenu.Separator)
}
if (!selected.isEmpty) {
val text = {
@@ -166,7 +169,7 @@
def apply = panel.fit_to_window()
}).peer
)
-
+
popup
}
}
--- a/src/Tools/Graphview/src/shapes.scala Mon Dec 10 21:28:01 2012 +0100
+++ b/src/Tools/Graphview/src/shapes.scala Mon Dec 10 21:55:57 2012 +0100
@@ -193,7 +193,7 @@
def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
{
val i = path.getPathIterator(null, 1.0)
- var seg = Array[Double](0,0,0,0,0,0)
+ val seg = Array[Double](0,0,0,0,0,0)
var p1 = (0.0, 0.0)
var p2 = (0.0, 0.0)
while (!i.isDone()) {
--- a/src/Tools/Graphview/src/visualizer.scala Mon Dec 10 21:28:01 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala Mon Dec 10 21:55:57 2012 +0100
@@ -17,6 +17,10 @@
class Visualizer(val model: Model)
{
+ visualizer =>
+
+ val parameters = new Parameters
+
object Coordinates
{
private var layout = Layout_Pendulum.empty_layout
@@ -82,7 +86,6 @@
}
}
- private val visualizer = this
object Drawer
{
def apply(g: Graphics2D, n: Option[String])
@@ -105,7 +108,7 @@
g.setRenderingHints(rendering_hints)
model.visible_edges().foreach(e => {
- apply(g, e, Parameters.arrow_heads, dummies)
+ apply(g, e, parameters.arrow_heads, dummies)
})
model.visible_nodes().foreach(l => {
@@ -153,7 +156,7 @@
def apply(key: String) = model.complete.get_node(key).name
}
- val font = new Font(Parameters.font_family, Font.BOLD, Parameters.font_size)
+ val font = new Font(parameters.font_family, Font.BOLD, parameters.font_size)
val rendering_hints =
new RenderingHints(