# HG changeset patch # User wenzelm # Date 1275061698 -7200 # Node ID 8b4617ad1593402ba4a661797d06888022bb1021 # Parent a60f88087ee1a5c3b5e69da8a74f318a35793724 reuse main view.font from jEdit; diff -r a60f88087ee1 -r 8b4617ad1593 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Fri May 28 16:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Fri May 28 17:48:18 2010 +0200 @@ -10,7 +10,7 @@ import isabelle._ import java.io.StringReader -import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics} +import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics} import java.awt.event.MouseEvent import java.util.logging.{Logger, Level} @@ -36,7 +36,11 @@ } -class HTML_Panel(system: Isabelle_System, initial_font_size: Int) extends HtmlPanel +class HTML_Panel( + system: Isabelle_System, + initial_font_family: String, + initial_font_size: Int) + extends HtmlPanel { /** Lobo setup **/ @@ -101,9 +105,9 @@ """ - private def template(font_size: Int): String = + private def template(font_family: String, font_size: Int): String = template_head + - "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" + + "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px }" + template_tail @@ -111,7 +115,7 @@ /* internal messages */ - private case class Resize(font_size: Int) + private case class Resize(font_family: String, font_size: Int) private case class Render(body: List[XML.Tree]) private case object Refresh @@ -120,22 +124,26 @@ /* internal state */ var current_font_metrics: FontMetrics = null + var current_font_family = "" var current_font_size: Int = 0 var current_margin: Int = 0 var current_body: List[XML.Tree] = Nil - def resize(font_size: Int) + def resize(font_family: String, font_size: Int) { + val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size))) val (font_metrics, margin) = Swing_Thread.now { - val metrics = getFontMetrics(system.get_font(lobo_px(raw_px(font_size)))) + val metrics = getFontMetrics(font) (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20) } if (current_font_metrics == null || + current_font_family != font_family || current_font_size != font_size || current_margin != margin) { current_font_metrics = font_metrics + current_font_family = font_family current_font_size = font_size current_margin = margin refresh() @@ -153,7 +161,8 @@ .map(t => XML.Elem(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE)), HTML.spans(t)))) val doc = builder.parse( - new InputSourceImpl(new StringReader(template(current_font_size)), "http://localhost")) + new InputSourceImpl( + new StringReader(template(current_font_family, current_font_size)), "http://localhost")) doc.removeChild(doc.getLastChild()) doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body))) Swing_Thread.later { setDocument(doc, rcontext) } @@ -162,11 +171,11 @@ /* main loop */ - resize(initial_font_size) + resize(initial_font_family, initial_font_size) loop { react { - case Resize(font_size) => resize(font_size) + case Resize(font_family, font_size) => resize(font_family, font_size) case Refresh => refresh() case Render(body) => render(body) case bad => System.err.println("main_actor: ignoring bad message " + bad) @@ -177,7 +186,7 @@ /* external methods */ - def resize(font_size: Int) { main_actor ! Resize(font_size) } + def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) } def refresh() { main_actor ! Refresh } def render(body: List[XML.Tree]) { main_actor ! Render(body) } } diff -r a60f88087ee1 -r 8b4617ad1593 src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 28 16:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 28 17:48:18 2010 +0200 @@ -24,7 +24,8 @@ { Swing_Thread.assert() - val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size())) + val html_panel = + new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) add(html_panel, BorderLayout.CENTER) @@ -40,7 +41,8 @@ private def handle_resize() { Swing_Thread.now { - html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100)) + html_panel.resize(Isabelle.font_family(), + scala.math.round(Isabelle.font_size() * zoom_factor / 100)) } } diff -r a60f88087ee1 -r 8b4617ad1593 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Fri May 28 16:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Fri May 28 17:48:18 2010 +0200 @@ -71,6 +71,11 @@ jEdit.setIntegerProperty(OPTION_PREFIX + name, value) } + + /* font */ + + def font_family(): String = jEdit.getProperty("view.font") + def font_size(): Float = (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)).toFloat / 100