tuned signature;
authorwenzelm
Wed, 31 Aug 2022 20:41:30 +0200
changeset 76024 dc1a950183a4
parent 76023 c7fed2fd52f5
child 76025 2ba535c2d2d8
tuned signature;
src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Aug 31 16:39:18 2022 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Aug 31 20:41:30 2022 +0200
@@ -55,7 +55,7 @@
   private val pretty_text_area = new Pretty_Text_Area(view)
   private val message_pane = new TabbedPane
 
-  def show_state(): Unit = GUI_Thread.later {
+  private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
     pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output)