clarified synchronized scope;

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 09 11:18:01 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 09 11:25:46 2014 +0200
@@ -110,16 +110,16 @@
 
   /* overlays */
 
-  private var overlays = Document.Overlays.empty
+  private val overlays = Synchronized(Document.Overlays.empty)
 
   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
-    synchronized { overlays(name) }
+    overlays.value(name)
 
   override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
-    synchronized { overlays = overlays.insert(command, fn, args) }
+    overlays.change(_.insert(command, fn, args))
 
   override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
-    synchronized { overlays = overlays.remove(command, fn, args) }
+    overlays.change(_.remove(command, fn, args))
 
 
   /* navigation */