# HG changeset patch
# User wenzelm
# Date 1372682251 -7200
# Node ID bf45606912e35eed3906f3f4b360af451a4fc709
# Parent  a1e09340c0f4e1ba3c6c95e3773cc6ecab061716
more robust delayed invocation;

diff -r a1e09340c0f4 -r bf45606912e3 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Jul 01 14:30:56 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Jul 01 14:37:31 2013 +0200
@@ -194,7 +194,7 @@
 
         if (e.getSource == text_area.getPainter) {
           Pretty_Tooltip.invoke(() =>
-            {
+            robust_body(()) {
               val rendering = get_rendering()
               val snapshot = rendering.snapshot
               if (!snapshot.is_outdated) {
@@ -217,7 +217,7 @@
                     }
                 }
               }
-            })
+          })
         }
       }
     }