# HG changeset patch
# User wenzelm
# Date 1670276576 -3600
# Node ID 1c1d7b3478b1334945dfdee0551742e2ccfddeed
# Parent  aef247025f071a7d12fb11f9916c3cbcd7e1fa52
tuned GUI behaviour;

diff -r aef247025f07 -r 1c1d7b3478b1 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Mon Dec 05 22:31:46 2022 +0100
+++ b/src/Pure/General/exn.scala	Mon Dec 05 22:42:56 2022 +0100
@@ -78,6 +78,12 @@
   def failure_rc(exn: Throwable): Int =
     isabelle.setup.Exn.failure_rc(exn)
 
+  def is_interrupt_exn[A](result: Result[A]): Boolean =
+    result match {
+      case Exn(exn) if is_interrupt(exn) => true
+      case _ => false
+    }
+
   def interruptible_capture[A](e: => A): Result[A] =
     try { Res(e) }
     catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
diff -r aef247025f07 -r 1c1d7b3478b1 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Mon Dec 05 22:31:46 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Mon Dec 05 22:42:56 2022 +0100
@@ -177,7 +177,8 @@
             val result = Document_Dockable.Result(output = List(msg))
             current_state.change(_ => Document_Dockable.State.finish(result))
             show_state()
-            show_page(output_page)
+
+            show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
             GUI_Thread.later { progress.load() }
           }
         st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)