# HG changeset patch # User wenzelm # Date 1543403150 -3600 # Node ID 71ef6e6da3dc92e852c9b8196890e0bb8d21319d # Parent acd0d72c560b0745a26d648460839f87d03ac298 prefer Isabelle_Fonts.sans (not mono) as derived GUI font; diff -r acd0d72c560b -r 71ef6e6da3dc src/Pure/GUI/gui.scala --- 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 diff -r acd0d72c560b -r 71ef6e6da3dc src/Tools/jEdit/src/debugger_dockable.scala --- 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("Eval") { diff -r acd0d72c560b -r 71ef6e6da3dc src/Tools/jEdit/src/graphview_dockable.scala --- 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 diff -r acd0d72c560b -r 71ef6e6da3dc src/Tools/jEdit/src/isabelle_sidekick.scala --- 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) diff -r acd0d72c560b -r 71ef6e6da3dc src/Tools/jEdit/src/pretty_text_area.scala --- 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 diff -r acd0d72c560b -r 71ef6e6da3dc src/Tools/jEdit/src/query_dockable.scala --- 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)) }