# HG changeset patch
# User wenzelm
# Date 1484220552 -3600
# Node ID b2e78c0ce5376fcaa33d84206a0f7bb73b87be8c
# Parent  e89f5ef32aa213942eac6d05a53833487554320b
more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;

diff -r e89f5ef32aa2 -r b2e78c0ce537 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Jan 12 11:20:40 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Jan 12 12:29:12 2017 +0100
@@ -41,11 +41,13 @@
 
   /* robust extension body */
 
+  def check_robust_body: Boolean =
+    GUI_Thread.require { buffer == text_area.getBuffer }
+
   def robust_body[A](default: A)(body: => A): A =
   {
     try {
-      GUI_Thread.require {}
-      if (buffer == text_area.getBuffer) body
+      if (check_robust_body) body
       else {
         Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
         default
diff -r e89f5ef32aa2 -r b2e78c0ce537 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Thu Jan 12 11:20:40 2017 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Thu Jan 12 12:29:12 2017 +0100
@@ -115,7 +115,8 @@
 
   private val delay_refresh =
     GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) {
-      doc_view.rich_text_area.robust_body(()) {
+      if (!doc_view.rich_text_area.check_robust_body) invoke()
+      else {
         JEdit_Lib.buffer_lock(buffer) {
           val rendering = doc_view.get_rendering()
           val overview = get_overview()