src/Tools/jEdit/src/document_view.scala
changeset 43417 83be997a11d6
parent 43414 f0770743b7ec
child 43419 6ed49c52d463
     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 **/