--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 23:09:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 23:36:06 2010 +0200
@@ -24,9 +24,7 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
- val html_panel =
- new HTML_Panel(Isabelle.system,
- Isabelle.font_size(), Isabelle.Int_Property("relative-margin"), null)
+ val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
add(html_panel, BorderLayout.CENTER)
@@ -43,8 +41,7 @@
html_panel.render(body)
}
- case Session.Global_Settings =>
- html_panel.init(Isabelle.font_size(), Isabelle.Int_Property("relative-margin"))
+ case Session.Global_Settings => html_panel.init(Isabelle.font_size())
case bad => System.err.println("output_actor: ignoring bad message " + bad)
}