# HG changeset patch # User wenzelm # Date 1419346838 -3600 # Node ID ec83638b6bfb25c1f86477251b04cc9316510613 # Parent dc41b77dcc8fe5cf889c58aca8071ce670a04eaf imitate font more carefully: err on smaller size; imitate HTML font, notably for Sidekick where short string is also shown as view status message; diff -r dc41b77dcc8f -r ec83638b6bfb src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Mon Dec 22 21:34:11 2014 +0100 +++ b/src/Pure/GUI/gui.scala Tue Dec 23 16:00:38 2014 +0100 @@ -222,8 +222,15 @@ def imitate_font(family: String, font: Font, scale: Double = 1.0): Font = { val font1 = new Font(family, font.getStyle, font.getSize) - val size = scale * (font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize) - font1.deriveFont(size.round.toInt) + val size = font_metrics(font).getHeight.toDouble / font_metrics(font1).getHeight * font.getSize + font1.deriveFont((scale * size).toInt) + } + + def imitate_font_css(family: String, font: Font, scale: Double = 1.0): String = + { + val font1 = new Font(family, font.getStyle, font.getSize) + val rel_size = font_metrics(font).getHeight.toDouble / font_metrics(font1).getHeight + "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;" } def transform_font(font: Font, transform: AffineTransform): Font = diff -r dc41b77dcc8f -r ec83638b6bfb src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Dec 22 21:34:11 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Dec 23 16:00:38 2014 +0100 @@ -12,7 +12,7 @@ import javax.swing.tree.DefaultMutableTreeNode import javax.swing.text.Position -import javax.swing.Icon +import javax.swing.{JLabel, Icon} import org.gjt.sp.jedit.Buffer import sidekick.{SideKickParser, SideKickParsedData, IAsset} @@ -32,12 +32,14 @@ class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset { + private val css = GUI.imitate_font_css(Font_Info.main_family(), (new JLabel).getFont) + protected var _name = text protected var _start = int_to_pos(range.start) protected var _end = int_to_pos(range.stop) override def getIcon: Icon = null override def getShortString: String = - "" + + "" + (if (keyword != "" && _name.startsWith(keyword)) "" + HTML.encode(keyword) + "" + HTML.encode(_name.substring(keyword.length)) else HTML.encode(_name)) + ""