# HG changeset patch
# User wenzelm
# Date 1407576346 -7200
# Node ID ea94d2aa62be57011a754e2a9734342722fc8cee
# Parent  28e17057b5456df290537b52fa76876595d3470d
clarified synchronized scope;

diff -r 28e17057b545 -r ea94d2aa62be src/Tools/jEdit/src/jedit_editor.scala
--- 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 */