src/Tools/jEdit/src/document_view.scala
changeset 43661 39fdbd814c7f
parent 43650 f00da558b78e
child 44378 81b4af4cfa5a
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 20:18:19 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 22:11:32 2011 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4    private def exit_popup() { html_popup.map(_.hide) }
     1.5  
     1.6    private val html_panel =
     1.7 -    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
     1.8 +    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
     1.9    html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
    1.10  
    1.11    private def html_panel_resize()