--- a/src/Tools/jEdit/src/document_view.scala Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Mon Jul 04 22:11:32 2011 +0200
@@ -143,7 +143,7 @@
private def exit_popup() { html_popup.map(_.hide) }
private val html_panel =
- new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+ new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
private def html_panel_resize()