--- a/src/Pure/GUI/gui.scala Wed Nov 28 11:43:06 2018 +0100
+++ b/src/Pure/GUI/gui.scala Wed Nov 28 12:05:50 2018 +0100
@@ -216,14 +216,18 @@
def line_metrics(font: Font): LineMetrics =
font.getLineMetrics("", new FontRenderContext(null, false, false))
- def imitate_font(font: Font, family: String, scale: Double = 1.0): Font =
+ def imitate_font(font: Font,
+ family: String = Isabelle_Fonts.sans,
+ scale: Double = 1.0): Font =
{
val font1 = new Font(family, font.getStyle, font.getSize)
val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt)
}
- def imitate_font_css(font: Font, family: String, scale: Double = 1.0): String =
+ def imitate_font_css(font: Font,
+ family: String = Isabelle_Fonts.sans,
+ scale: Double = 1.0): String =
{
val font1 = new Font(family, font.getStyle, font.getSize)
val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
--- a/src/Tools/jEdit/src/debugger_dockable.scala Wed Nov 28 11:43:06 2018 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Wed Nov 28 12:05:50 2018 +0100
@@ -240,7 +240,7 @@
}
setColumns(20)
setToolTipText(context_label.tooltip)
- setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
+ setFont(GUI.imitate_font(getFont, scale = 1.2))
}
private val expression_label = new Label("ML:") {
@@ -258,7 +258,7 @@
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(expression_label.tooltip)
- setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
+ setFont(GUI.imitate_font(getFont, scale = 1.2))
}
private val eval_button = new Button("<html><b>Eval</b></html>") {
--- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Nov 28 11:43:06 2018 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Nov 28 12:05:50 2018 +0100
@@ -81,8 +81,8 @@
if (editor_style) Font_Info.main(PIDE.options.real("graphview_font_scale")).font
else
GUI.imitate_font(Font_Info.main().font,
- options.string("graphview_font_family"),
- options.real("graphview_font_scale"))
+ family = options.string("graphview_font_family"),
+ scale = options.real("graphview_font_scale"))
override def foreground_color =
if (editor_style) view.getTextArea.getPainter.getForeground
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Nov 28 11:43:06 2018 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Nov 28 12:05:50 2018 +0100
@@ -32,7 +32,7 @@
class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
{
- private val css = GUI.imitate_font_css((new JLabel).getFont, Font_Info.main_family())
+ private val css = GUI.imitate_font_css((new JLabel).getFont)
protected var _name = text
protected var _start = int_to_pos(range.start)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Nov 28 11:43:06 2018 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Nov 28 12:05:50 2018 +0100
@@ -201,7 +201,7 @@
})
setColumns(20)
setToolTipText(search_label.tooltip)
- setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
+ setFont(GUI.imitate_font(getFont, scale = 1.2))
})
private val search_field_foreground = search_field.foreground
--- a/src/Tools/jEdit/src/query_dockable.scala Wed Nov 28 11:43:06 2018 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Wed Nov 28 12:05:50 2018 +0100
@@ -50,7 +50,7 @@
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(tooltip)
- setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
+ setFont(GUI.imitate_font(getFont, scale = 1.2))
}