# 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,