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