# HG changeset patch
# User wenzelm
# Date 1350740808 -7200
# Node ID 44658062d822c71a695577c6697f72ebfcd485f8
# Parent  fc2e3b9d485265fd54f755af6eced661557bce88
more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;

diff -r fc2e3b9d4852 -r 44658062d822 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Oct 20 15:45:40 2012 +0200
+++ b/src/Pure/System/options.scala	Sat Oct 20 15:46:48 2012 +0200
@@ -198,32 +198,36 @@
 
   /* internal lookup and update */
 
-  val bool = new Object
+  class Bool_Access
   {
     def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
     def update(name: String, x: Boolean): Options =
       put(name, Options.Bool, Properties.Value.Boolean(x))
   }
+  val bool = new Bool_Access
 
-  val int = new Object
+  class Int_Access
   {
     def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
     def update(name: String, x: Int): Options =
       put(name, Options.Int, Properties.Value.Int(x))
   }
+  val int = new Int_Access
 
-  val real = new Object
+  class Real_Access
   {
     def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
     def update(name: String, x: Double): Options =
       put(name, Options.Real, Properties.Value.Double(x))
   }
+  val real = new Real_Access
 
-  val string = new Object
+  class String_Access
   {
     def apply(name: String): String = get(name, Options.String, s => Some(s))
     def update(name: String, x: String): Options = put(name, Options.String, x)
   }
+  val string = new String_Access
 
 
   /* external updates */
@@ -363,7 +367,7 @@
     options = options + (name, x)
   }
 
-  val bool = new Object
+  class Bool_Access
   {
     def apply(name: String): Boolean = options.bool(name)
     def update(name: String, x: Boolean)
@@ -372,8 +376,9 @@
       options = options.bool.update(name, x)
     }
   }
+  val bool = new Bool_Access
 
-  val int = new Object
+  class Int_Access
   {
     def apply(name: String): Int = options.int(name)
     def update(name: String, x: Int)
@@ -382,8 +387,9 @@
       options = options.int.update(name, x)
     }
   }
+  val int = new Int_Access
 
-  val real = new Object
+  class Real_Access
   {
     def apply(name: String): Double = options.real(name)
     def update(name: String, x: Double)
@@ -392,8 +398,9 @@
       options = options.real.update(name, x)
     }
   }
+  val real = new Real_Access
 
-  val string = new Object
+  class String_Access
   {
     def apply(name: String): String = options.string(name)
     def update(name: String, x: String)
@@ -402,5 +409,6 @@
       options = options.string.update(name, x)
     }
   }
+  val string = new String_Access
 }
 
diff -r fc2e3b9d4852 -r 44658062d822 src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Sat Oct 20 15:45:40 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Sat Oct 20 15:46:48 2012 +0200
@@ -67,7 +67,7 @@
   
   def apply_layout() = visualizer.Coordinates.layout()  
 
-  private val paint_panel = new Panel {    
+  private class Paint_Panel extends Panel {
     def set_preferred_size() {
         val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
         val s = Transform.scale
@@ -86,6 +86,7 @@
       visualizer.Drawer.paint_all_visible(g, true)
     }
   }
+  private val paint_panel = new Paint_Panel
   contents = paint_panel
   
   listenTo(keys)