# HG changeset patch
# User wenzelm
# Date 1730976381 -3600
# Node ID 76f74ac9edee8035f3ea8817e2d1f42184ff0ef8
# Parent  83012fe972820105fa215abfc9e0ce21d2999d3f
tuned;

diff -r 83012fe97282 -r 76f74ac9edee src/Tools/jEdit/src/completion_popup.scala
--- 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
 
diff -r 83012fe97282 -r 76f74ac9edee src/Tools/jEdit/src/font_info.scala
--- 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 */
diff -r 83012fe97282 -r 76f74ac9edee src/Tools/jEdit/src/pretty_text_area.scala
--- 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(
diff -r 83012fe97282 -r 76f74ac9edee src/Tools/jEdit/src/symbols_dockable.scala
--- 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 */