# HG changeset patch
# User wenzelm
# Date 1285164983 -7200
# Node ID 5638fe4f0843565de24399f5784d8a5707c86e34
# Parent  a43a723753e6b353e4f6ae12eecc332a20cdae7b
tuned signature;

diff -r a43a723753e6 -r 5638fe4f0843 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Sep 22 16:04:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Sep 22 16:16:23 2010 +0200
@@ -24,7 +24,7 @@
 {
   Swing_Thread.require()
 
-  val html_panel =
+  private val html_panel =
     new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   set_content(html_panel)
 
@@ -137,7 +137,7 @@
   }
   update.tooltip = "Update display according to the command at cursor position"
 
-  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
+  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
   add(controls.peer, BorderLayout.NORTH)
 
   handle_update()