--- a/src/Pure/System/options.scala Thu Apr 04 18:25:47 2013 +0200
+++ b/src/Pure/System/options.scala Thu Apr 04 18:44:22 2013 +0200
@@ -358,69 +358,48 @@
class Options_Variable
{
- // owned by Swing thread
- @volatile private var options = Options.empty
+ private var options = Options.empty
- def value: Options = options
- def update(new_options: Options)
- {
- Swing_Thread.require()
- options = new_options
- }
+ def value: Options = synchronized { options }
+ def update(new_options: Options): Unit = synchronized { options = new_options }
- def + (name: String, x: String)
- {
- Swing_Thread.require()
- options = options + (name, x)
- }
+ def + (name: String, x: String): Unit = synchronized { options = options + (name, x) }
class Bool_Access
{
- def apply(name: String): Boolean = options.bool(name)
- def update(name: String, x: Boolean)
- {
- Swing_Thread.require()
- options = options.bool.update(name, x)
- }
+ def apply(name: String): Boolean = synchronized { options.bool(name) }
+ def update(name: String, x: Boolean): Unit =
+ synchronized { options = options.bool.update(name, x) }
}
val bool = new Bool_Access
class Int_Access
{
- def apply(name: String): Int = options.int(name)
- def update(name: String, x: Int)
- {
- Swing_Thread.require()
- options = options.int.update(name, x)
- }
+ def apply(name: String): Int = synchronized { options.int(name) }
+ def update(name: String, x: Int): Unit =
+ synchronized { options = options.int.update(name, x) }
}
val int = new Int_Access
class Real_Access
{
- def apply(name: String): Double = options.real(name)
- def update(name: String, x: Double)
- {
- Swing_Thread.require()
- options = options.real.update(name, x)
- }
+ def apply(name: String): Double = synchronized { options.real(name) }
+ def update(name: String, x: Double): Unit =
+ synchronized { options = options.real.update(name, x) }
}
val real = new Real_Access
class String_Access
{
- def apply(name: String): String = options.string(name)
- def update(name: String, x: String)
- {
- Swing_Thread.require()
- options = options.string.update(name, x)
- }
+ def apply(name: String): String = synchronized { options.string(name) }
+ def update(name: String, x: String): Unit =
+ synchronized { options = options.string.update(name, x) }
}
val string = new String_Access
class Seconds_Access
{
- def apply(name: String): Time = options.seconds(name)
+ def apply(name: String): Time = synchronized { options.seconds(name) }
}
val seconds = new Seconds_Access
}