--- 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) &&