1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 09 11:18:01 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 09 11:25:46 2014 +0200
     1.3 @@ -110,16 +110,16 @@
     1.4  
     1.5    /* overlays */
     1.6  
     1.7 -  private var overlays = Document.Overlays.empty
     1.8 +  private val overlays = Synchronized(Document.Overlays.empty)
     1.9  
    1.10    override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    1.11 -    synchronized { overlays(name) }
    1.12 +    overlays.value(name)
    1.13  
    1.14    override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    1.15 -    synchronized { overlays = overlays.insert(command, fn, args) }
    1.16 +    overlays.change(_.insert(command, fn, args))
    1.17  
    1.18    override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    1.19 -    synchronized { overlays = overlays.remove(command, fn, args) }
    1.20 +    overlays.change(_.remove(command, fn, args))
    1.21  
    1.22  
    1.23    /* navigation */