# HG changeset patch
# User wenzelm
# Date 1365093862 -7200
# Node ID 7c39677f9ea05fe285588a673f9ae9ed62a41271
# Parent  95b7da3430d49bca9131344583d94da8e17941ec
more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT);

diff -r 95b7da3430d4 -r 7c39677f9ea0 src/Pure/System/options.scala
--- 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
 }