tuned GUI behaviour;

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

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