# HG changeset patch # User wenzelm # Date 1274348681 -7200 # Node ID 485c5e478ab6ae2ba527850f308a9eb20b07fa71 # Parent ccb8da7f76e6d3ce63130306fbb95cfa5a91e690 tuned; diff -r ccb8da7f76e6 -r 485c5e478ab6 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 11:36:30 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 11:44:41 2010 +0200 @@ -23,7 +23,6 @@ import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl} import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext} -import scala.io.Source import scala.actors.Actor._ @@ -39,7 +38,7 @@ class HTML_Panel( - sys: Isabelle_System, + system: Isabelle_System, initial_font_size: Int, handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel { @@ -68,9 +67,9 @@ @@ -80,7 +79,7 @@ } private def font_metrics(font_size: Int): FontMetrics = - Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) } + Swing_Thread.now { getFontMetrics(system.get_font(font_size)) } private def panel_width(font_size: Int): Int = Swing_Thread.now {