# HG changeset patch
# User wenzelm
# Date 1289416915 -3600
# Node ID 576b88b1dce9fd7d187da28b7c0a028d8fa14752
# Parent  a6db1a68fe3c287538771c3d70db1660b535800d
added buffer_text convenience, with explicit locking;

diff -r a6db1a68fe3c -r 576b88b1dce9 src/Tools/jEdit/src/jedit/document_model.scala
--- 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()
diff -r a6db1a68fe3c -r 576b88b1dce9 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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))
diff -r a6db1a68fe3c -r 576b88b1dce9 src/Tools/jEdit/src/jedit/plugin.scala
--- 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 */