added buffer_text convenience, with explicit locking;

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Nov 10 17:53:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Nov 10 20:21:55 2010 +0100
@@ -219,7 +219,7 @@
     buffer.setTokenMarker(token_marker)
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
-    pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength))
+    pending_edits += Text.Edit.insert(0, Isabelle.buffer_text(buffer))
   }
 
   def refresh()

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 17:53:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 20:21:55 2010 +0100
@@ -137,8 +137,7 @@
         case _ => Nil
       }
 
-    val buffer = model.buffer
-    val text = Isabelle.buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+    val text = Isabelle.buffer_text(model.buffer)
     val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
 
     make_tree(0, structure) foreach (node => data.root.add(node))

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Nov 10 17:53:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Nov 10 20:21:55 2010 +0100
@@ -147,6 +147,9 @@
   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
     Swing_Thread.now { buffer_lock(buffer) { body } }
 
+  def buffer_text(buffer: JEditBuffer): String =
+    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+
 
   /* dockable windows */