# HG changeset patch # User wenzelm # Date 1273527407 -7200 # Node ID c8deab86617401869c366636a7e4a745fa4cb5a4 # Parent 076eded99ef768448f92e0f40532c5684cb21380 font size re-adjustment according to Lobo internals; diff -r 076eded99ef7 -r c8deab866174 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Mon May 10 22:29:27 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Mon May 10 23:36:47 2010 +0200 @@ -10,7 +10,7 @@ import isabelle._ import java.io.StringReader -import java.awt.{BorderLayout, Dimension} +import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit} import java.awt.event.MouseEvent import javax.swing.{JButton, JPanel, JScrollPane} @@ -56,6 +56,15 @@ } private def template(font_size: Int): String = + { + // re-adjustment according to org.lobobrowser.html.style.HtmlValues.getFontSize + val dpi = + if (GraphicsEnvironment.isHeadless()) 72 + else Toolkit.getDefaultToolkit().getScreenResolution() + + val size0 = font_size * dpi / 96 + val size = if (size0 * 96 / dpi == font_size) size0 else size0 + 1 + """ @@ -65,13 +74,14 @@ """ + try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" + try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" + - "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" + + "body { font-family: " + sys.font_family + "; font-size: " + size + "px }" + """ """ + } /* actor with local state */