more precise imitation of original TextAreaPainter: no locking;
authorwenzelm
Thu Jun 16 23:35:37 2011 +0200 (2011-06-16 ago)
changeset 4341783be997a11d6
parent 43416 e730cdd97dcf
child 43418 c69e9fbb81a8
more precise imitation of original TextAreaPainter: no locking;
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 23:16:06 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 23:35:37 2011 +0200
     1.3 @@ -72,15 +72,17 @@
     1.4    /** robust extension body **/
     1.5  
     1.6    def robust_body[A](default: A)(body: => A): A =
     1.7 -    Swing_Thread.now {
     1.8 -      try {
     1.9 -        Isabelle.buffer_lock(model.buffer) {
    1.10 -          if (model.buffer == text_area.getBuffer) body
    1.11 -          else default
    1.12 -        }
    1.13 +  {
    1.14 +    try {
    1.15 +      Swing_Thread.require()
    1.16 +      if (model.buffer == text_area.getBuffer) body
    1.17 +      else {
    1.18 +        // FIXME Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
    1.19 +        default
    1.20        }
    1.21 -      catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
    1.22      }
    1.23 +    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
    1.24 +  }
    1.25  
    1.26  
    1.27    /** token handling **/