# HG changeset patch
# User wenzelm
# Date 1348049440 -7200
# Node ID 491363c6feb4dcd95d27d9d27e420c2abb745110
# Parent  28bd0709443aeecababf51821adf0b0ceadf9694
more robust GUI component handlers;

diff -r 28bd0709443a -r 491363c6feb4 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Sep 18 21:16:48 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Sep 19 12:10:40 2012 +0200
@@ -97,6 +97,7 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
+      // no robust_body
       model.update_perspective()
     }
   }
diff -r 28bd0709443a -r 491363c6feb4 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Sep 18 21:16:48 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Sep 19 12:10:40 2012 +0200
@@ -127,35 +127,39 @@
   private def active_reset(): Unit = active_areas.foreach(_.reset)
 
   private val focus_listener = new FocusAdapter {
-    override def focusLost(e: FocusEvent) { active_reset() }
+    override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
   }
 
   private val window_listener = new WindowAdapter {
-    override def windowIconified(e: WindowEvent) { active_reset() }
-    override def windowDeactivated(e: WindowEvent) { active_reset() }
+    override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
+    override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
   }
 
   private val mouse_listener = new MouseAdapter {
     override def mouseClicked(e: MouseEvent) {
-      hyperlink_area.info match {
-        case Some(Text.Info(range, link)) => link.follow(view)
-        case None =>
+      robust_body(()) {
+        hyperlink_area.info match {
+          case Some(Text.Info(range, link)) => link.follow(view)
+          case None =>
+        }
       }
     }
   }
 
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseMoved(e: MouseEvent) {
-      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
-      if (control && !buffer.isLoading) {
-        JEdit_Lib.buffer_lock(buffer) {
-          val rendering = get_rendering()
-          val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
-          val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
-          active_areas.foreach(_.update_rendering(rendering, mouse_range))
+      robust_body(()) {
+        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+        if (control && !buffer.isLoading) {
+          JEdit_Lib.buffer_lock(buffer) {
+            val rendering = get_rendering()
+            val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
+            val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
+            active_areas.foreach(_.update_rendering(rendering, mouse_range))
+          }
         }
+        else active_reset()
       }
-      else active_reset()
     }
   }