sporadic locking of jEdit buffer;

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 23 16:53:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 23 17:35:47 2010 +0200
@@ -106,8 +106,27 @@
           Swing_Thread.now {
             // FIXME cover doc states as well!!?
             val snapshot = model.snapshot()
-            if (changed.exists(snapshot.node.commands.contains))
-              full_repaint(snapshot, changed)
+            val buffer = model.buffer
+            Isabelle.buffer_read_lock(buffer) {
+              if (changed.exists(snapshot.node.commands.contains)) {
+                var visible_change = false
+
+                for ((command, start) <- snapshot.node.command_starts) {
+                  if (changed(command)) {
+                    val stop = start + command.length
+                    val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+                    val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
+                    if (line2 >= text_area.getFirstLine &&
+                        line1 <= text_area.getFirstLine + text_area.getVisibleLines)
+                      visible_change = true
+                    text_area.invalidateLineRange(line1, line2)
+                  }
+                }
+                if (visible_change) model.buffer.propertiesChanged()
+
+                overview.repaint()  // FIXME paint here!?
+              }
+            }
           }
 
         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
@@ -115,29 +134,6 @@
     }
   }
 
-  def full_repaint(snapshot: Document.Snapshot, changed: Set[Command])
-  {
-    Swing_Thread.require()
-
-    val buffer = model.buffer
-    var visible_change = false
-
-    for ((command, start) <- snapshot.node.command_starts) {
-      if (changed(command)) {
-        val stop = start + command.length
-        val line1 = buffer.getLineOfOffset(snapshot.convert(start))
-        val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
-        if (line2 >= text_area.getFirstLine &&
-            line1 <= text_area.getFirstLine + text_area.getVisibleLines)
-          visible_change = true
-        text_area.invalidateLineRange(line1, line2)
-      }
-    }
-    if (visible_change) model.buffer.propertiesChanged()
-
-    overview.repaint()  // FIXME paint here!?
-  }
-
 
   /* text_area_extension */
 
@@ -269,20 +265,23 @@
     override def paintComponent(gfx: Graphics)
     {
       super.paintComponent(gfx)
+      Swing_Thread.assert()
       val buffer = model.buffer
-      val snapshot = model.snapshot()
-      val saved_color = gfx.getColor  // FIXME needed!?
-      try {
-        for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
-          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
-          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
-          val y = line_to_y(line1)
-          val height = HEIGHT * (line2 - line1)
-          gfx.setColor(Document_View.choose_color(snapshot, command))
-          gfx.fillRect(0, y, getWidth - 1, height)
+      Isabelle.buffer_read_lock(buffer) {
+        val snapshot = model.snapshot()
+        val saved_color = gfx.getColor  // FIXME needed!?
+        try {
+          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
+            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+            val y = line_to_y(line1)
+            val height = HEIGHT * (line2 - line1)
+            gfx.setColor(Document_View.choose_color(snapshot, command))
+            gfx.fillRect(0, y, getWidth - 1, height)
+          }
         }
+        finally { gfx.setColor(saved_color) }
       }
-      finally { gfx.setColor(saved_color) }
     }
 
     private def line_to_y(line: Int): Int =

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Aug 23 16:53:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Aug 23 17:35:47 2010 +0200
@@ -40,6 +40,7 @@
 {
   def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
   {
+    // FIXME lock buffer (!??)
     Swing_Thread.assert()
     Document_Model(buffer) match {
       case Some(model) =>

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Aug 23 16:53:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Aug 23 17:35:47 2010 +0200
@@ -44,7 +44,7 @@
 
     stopped = false
 
-    // FIXME lock buffer !??
+    // FIXME lock buffer (!??)
     val data = new SideKickParsedData(buffer.getName)
     val root = data.root
     data.getAsset(root).setEnd(buffer.getLength)
@@ -66,6 +66,7 @@
 
   override def complete(pane: EditPane, caret: Int): SideKickCompletion =
   {
+    // FIXME lock buffer (!?)
     val buffer = pane.getBuffer
 
     val line = buffer.getLineOfOffset(caret)

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon Aug 23 16:53:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Mon Aug 23 17:35:47 2010 +0200
@@ -118,6 +118,12 @@
   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
     jedit_text_areas().filter(_.getBuffer == buffer)
 
+  def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A =
+  {
+    try { buffer.readLock(); body }
+    finally { buffer.readUnlock() }
+  }
+
 
   /* dockable windows */