more robust delayed invocation;

--- 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 @@
                     }
                 }
               }
-            })
+          })
         }
       }
     }