more precise imitation of original TextAreaPainter: no locking;

--- 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 **/