# HG changeset patch # User wenzelm # Date 1355172957 -3600 # Node ID bad1a1ca61e1e16be3e384ce0b5e0094aab43e18 # Parent a5930c929b1eedc950de3a44d9c6f0bb942abf70 separate instance of class Parameters for each Main_Panel -- avoid global program state; misc tuning; diff -r a5930c929b1e -r bad1a1ca61e1 src/Tools/Graphview/src/main_panel.scala --- 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.encode(Pretty.string_of(body)) + "
"
 
-  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 !?
   }
diff -r a5930c929b1e -r bad1a1ca61e1 src/Tools/Graphview/src/mutator.scala
--- 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)
diff -r a5930c929b1e -r bad1a1ca61e1 src/Tools/Graphview/src/mutator_dialog.scala
--- 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]()
 
diff -r a5930c929b1e -r bad1a1ca61e1 src/Tools/Graphview/src/parameters.scala
--- 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
 }
diff -r a5930c929b1e -r bad1a1ca61e1 src/Tools/Graphview/src/popups.scala
--- 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
   }
 }
diff -r a5930c929b1e -r bad1a1ca61e1 src/Tools/Graphview/src/shapes.scala
--- 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()) {
diff -r a5930c929b1e -r bad1a1ca61e1 src/Tools/Graphview/src/visualizer.scala
--- 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(