# HG changeset patch
# User wenzelm
# Date 1661971290 -7200
# Node ID dc1a950183a4d8a033acbb2c1abce293298e9834
# Parent  c7fed2fd52f5aeff599cfa83101d0a339f932bbb
tuned signature;

diff -r c7fed2fd52f5 -r dc1a950183a4 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)