diff -r 467f45e79ff9 -r 6d847e27cafc src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Mon Jan 16 20:40:42 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Mon Jan 16 20:57:38 2023 +0100 @@ -182,7 +182,7 @@ GUI_Thread.later { refresh_theories() show_state() - show_page(theories_page) + show_page(input_page) } } catch { @@ -247,7 +247,7 @@ finish_process(Pretty.separate(msgs)) show_state() - show_page(if (Exn.is_interrupt_exn(result)) theories_page else output_page) + show_page(if (Exn.is_interrupt_exn(result)) input_page else output_page) } case _ => } @@ -325,8 +325,8 @@ theories.refresh() } - private val theories_page = - new TabbedPane.Page("Theories", new BorderPanel { + private val input_page = + new TabbedPane.Page("Input", new BorderPanel { layout(theories_controls) = BorderPanel.Position.North layout(theories.gui) = BorderPanel.Position.Center }, "Selection and status of document theories") @@ -338,9 +338,9 @@ new TabbedPane.Page("Output", new BorderPanel { layout(output_controls) = BorderPanel.Position.North layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center - }, "Output from build process") + }, "Results from document build process") - message_pane.pages ++= List(theories_page, output_page) + message_pane.pages ++= List(input_page, output_page) set_content(message_pane)