src/Tools/jEdit/src/jedit/output_dockable.scala
changeset 37164 8b4617ad1593
parent 37132 10ef4da1c314
child 37372 babe498016e8
     1.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 28 16:01:25 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 28 17:48:18 2010 +0200
     1.3 @@ -24,7 +24,8 @@
     1.4  {
     1.5    Swing_Thread.assert()
     1.6  
     1.7 -  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
     1.8 +  val html_panel =
     1.9 +    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    1.10    add(html_panel, BorderLayout.CENTER)
    1.11  
    1.12  
    1.13 @@ -40,7 +41,8 @@
    1.14    private def handle_resize()
    1.15    {
    1.16      Swing_Thread.now {
    1.17 -      html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    1.18 +      html_panel.resize(Isabelle.font_family(),
    1.19 +        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    1.20      }
    1.21    }
    1.22