# HG changeset patch
# User wenzelm
# Date 1308260137 -7200
# Node ID 83be997a11d6604d2739cff33b91a47b62e46cf0
# Parent  e730cdd97dcfa7caacb7c401d5f20cf4ef5fc206
more precise imitation of original TextAreaPainter: no locking;

diff -r e730cdd97dcf -r 83be997a11d6 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 23:16:06 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 23:35:37 2011 +0200
@@ -72,15 +72,17 @@
   /** robust extension body **/
 
   def robust_body[A](default: A)(body: => A): A =
-    Swing_Thread.now {
-      try {
-        Isabelle.buffer_lock(model.buffer) {
-          if (model.buffer == text_area.getBuffer) body
-          else default
-        }
+  {
+    try {
+      Swing_Thread.require()
+      if (model.buffer == text_area.getBuffer) body
+      else {
+        // FIXME Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
+        default
       }
-      catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
     }
+    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
+  }
 
 
   /** token handling **/