# HG changeset patch # User wenzelm # Date 1355256338 -3600 # Node ID 8cc351df4a232f187cf0162ca28a856c5d357c9b # Parent 6ee044e2d1a7b815a678f2ee01afb3cf72c60a00 just one class with parameters; diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/lib/Tools/graphview --- 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" diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/src/main_panel.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.encode(Pretty.string_of(body)) + "
"
 
   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()
       }
     }
diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/src/mutator.scala
--- 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)
diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/src/mutator_dialog.scala
--- 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))
       )
     }
diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/src/parameters.scala
--- 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)
-    }
-  }
-}
diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/src/popups.scala
--- 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)
         }
       }
 
diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/src/shapes.scala
--- 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)
     }
 
diff -r 6ee044e2d1a7 -r 8cc351df4a23 src/Tools/Graphview/src/visualizer.scala
--- 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