--- a/src/Tools/jEdit/src/font_info.scala Thu Nov 07 12:08:32 2024 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Thu Nov 07 12:17:18 2024 +0100
@@ -31,8 +31,8 @@
def main_size(scale: Double = 1.0): Float =
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 = scale))
+ def main(scale: Double = 1.0, zoom: GUI.Zoom = null): Font_Info =
+ Font_Info(main_family(), main_size(if (zoom == null) scale else scale * zoom.scale))
/* incremental size change */