--- 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()