# HG changeset patch # User wenzelm # Date 1730978238 -3600 # Node ID 75a2c6af8a026bdc2cb08988231f0d3b750de088 # Parent 5e8287d34295dc022279c9485c937f64124cff19 clarified signature; diff -r 5e8287d34295 -r 75a2c6af8a02 src/Tools/jEdit/src/font_info.scala --- 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 */ diff -r 5e8287d34295 -r 75a2c6af8a02 src/Tools/jEdit/src/pretty_text_area.scala --- 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,