tuned signature;
authorwenzelm
Wed, 22 Sep 2010 16:16:23 +0200
changeset 39592 5638fe4f0843
parent 39591 a43a723753e6
child 39593 1a34187f0b97
tuned signature;
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()