clarified GUI: avoid odd jumping pages on "Cancel";
authorwenzelm
Tue, 31 Jan 2023 17:46:16 +0100
changeset 77155 6840013a791a
parent 77154 dd9bde3d839e
child 77156 e3a7d3668629
clarified GUI: avoid odd jumping pages on "Cancel";
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
     }