tuned GUI;
authorwenzelm
Mon, 16 Jan 2023 20:57:38 +0100
changeset 76996 6d847e27cafc
parent 76995 467f45e79ff9
child 76997 d481dc154310
tuned GUI;
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)