src/Tools/jEdit/src/pretty_text_area.scala

       if (result.nonEmpty) {
         result += Command.rich_text(body = Pretty.Separator, id = Document_ID.make())
       }
       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
   }
 }
 

             try {
               val rich_texts = Pretty_Text_Area.format_rich_texts(output, metric, results)
               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) &&
               output == current_output &&
               snapshot == current_base_snapshot &&