# HG changeset patch
# User wenzelm
# Date 1675183576 -3600
# Node ID 6840013a791aef9e901f587eaed7f725421db172
# Parent  dd9bde3d839e66455f7c3081f1e0f2fe9355da7e
clarified GUI: avoid odd jumping pages on "Cancel";

diff -r dd9bde3d839e -r 6840013a791a src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:35:59 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:46:16 2023 +0100
@@ -251,7 +251,7 @@
         finish_process(Pretty.separate(msgs))
 
         show_state()
-        show_page(if (Exn.is_interrupt_exn(result)) input_page else output_page)
+        show_page(output_page)
       }
       true
     }