author | wenzelm |
Tue, 31 Jan 2023 17:21:46 +0100 | |
changeset 77153 | 0bb95bcf804e |
parent 77152 | 4c9296390f20 |
child 77154 | dd9bde3d839e |
--- a/src/Tools/jEdit/src/document_dockable.scala Tue Jan 31 17:17:07 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Tue Jan 31 17:21:46 2023 +0100 @@ -231,7 +231,9 @@ else if (document_session.is_pending) false else { run_process(reset_pending = true) { progress => + output_process(progress) show_page(output_page) + val result = Exn.capture { document_build(document_session, progress) } val msgs = result match {