--- 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 */
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 07 12:08:32 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 07 12:17:18 2024 +0100
@@ -122,10 +122,8 @@
refresh()
}
- def zoom(zoom: GUI.Zoom): Unit = {
- val percent = if (zoom == null) 100 else zoom.percent
- resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale") * percent / 100))
- }
+ def zoom(zoom: GUI.Zoom): Unit =
+ resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom))
def update(
base_snapshot: Document.Snapshot,