--- a/src/Tools/jEdit/src/completion_popup.scala Thu Nov 07 11:35:39 2024 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Thu Nov 07 11:46:21 2024 +0100
@@ -230,7 +230,7 @@
def open_popup(result: Completion.Result): Unit = {
val font =
painter.getFont.deriveFont(
- Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
+ Font_Info.main_size(scale = PIDE.options.real("jedit_popup_font_scale")))
val range = result.range
--- a/src/Tools/jEdit/src/font_info.scala Thu Nov 07 11:35:39 2024 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Thu Nov 07 11:46:21 2024 +0100
@@ -32,7 +32,7 @@
restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
def main(scale: Double = 1.0): Font_Info =
- Font_Info(main_family(), main_size(scale))
+ Font_Info(main_family(), main_size(scale = scale))
/* incremental size change */
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 07 11:35:39 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 07 11:46:21 2024 +0100
@@ -124,7 +124,7 @@
def zoom(zoom: GUI.Zoom): Unit = {
val factor = if (zoom == null) 100 else zoom.factor
- resize(Font_Info.main(PIDE.options.real("jedit_font_scale") * factor / 100))
+ resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale") * factor / 100))
}
def update(
--- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Nov 07 11:35:39 2024 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Thu Nov 07 11:46:21 2024 +0100
@@ -18,7 +18,7 @@
class Symbols_Dockable(view: View, position: String) extends Dockable(view, position) {
private def font_size: Int =
- Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
+ Font_Info.main_size(scale = PIDE.options.real("jedit_font_scale")).round
/* abbrevs */