imitate font more carefully: err on smaller size;
imitate HTML font, notably for Sidekick where short string is also shown as view status message;
--- 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 =
--- 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 =
- "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
+ "<html><span style=\"" + css + "\">" +
(if (keyword != "" && _name.startsWith(keyword))
"<b>" + HTML.encode(keyword) + "</b>" + HTML.encode(_name.substring(keyword.length))
else HTML.encode(_name)) + "</span></html>"