# HG changeset patch
# User wenzelm
# Date 1731235103 -3600
# Node ID 1e3dfb722ee6e2c0c5c94f0d5029062e85a9a63d
# Parent  ed4ff84e9b2177b921de950d6cb63f3439887dfa
more reactive interrupts (via Future.cancel);

diff -r ed4ff84e9b21 -r 1e3dfb722ee6 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 21:34:38 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 11:38:23 2024 +0100
@@ -41,6 +41,8 @@
       }
       val body = Pretty.formatted(List(msg), margin = metric.margin, metric = metric)
       result += Command.rich_text(body = body, id = Markup.Serial.get(msg.markup.properties))
+
+      Exn.Interrupt.expose()
     }
     result.toList
   }
@@ -119,8 +121,11 @@
               val rendering = JEdit_Rendering(snapshot, rich_texts)
               (Command.full_source(rich_texts), rendering)
             }
-            catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
-          Exn.Interrupt.expose()
+            catch {
+              case exn: Throwable if !Exn.is_interrupt(exn) =>
+                Log.log(Log.ERROR, this, exn)
+                throw exn
+            }
 
           GUI_Thread.later {
             if (metric == JEdit_Lib.font_metric(getPainter) &&