# HG changeset patch
# User wenzelm
# Date 1730982640 -3600
# Node ID 5c8c94d5211a3347393d4c476c05b156b5347ce4
# Parent  69c61216c87ac534d30e436fb47b7b45544646e6
clarified signature: more accurate types;

diff -r 69c61216c87a -r 5c8c94d5211a src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Thu Nov 07 13:26:31 2024 +0100
+++ b/src/Tools/jEdit/src/font_info.scala	Thu Nov 07 13:30:40 2024 +0100
@@ -31,9 +31,11 @@
   def main_size(scale: Double = 1.0): Float =
     restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
 
-  def main(scale: Double = 1.0, zoom: GUI.Zoom = null): Font_Info =
+  def main(scale: Double = 1.0, zoom: Zoom = null): Font_Info =
     Font_Info(main_family(), main_size(if (zoom == null) scale else scale * zoom.scale))
 
+  class Zoom extends GUI.Zoom { tooltip = "Zoom factor for output font size" }
+
 
   /* incremental size change */
 
@@ -76,11 +78,6 @@
       change_size(_ => size)
     }
   }
-
-
-  /* zoom */
-
-  class Zoom extends GUI.Zoom { tooltip = "Zoom factor for output font size" }
 }
 
 sealed case class Font_Info(family: String, size: Float) {
diff -r 69c61216c87a -r 5c8c94d5211a src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 13:26:31 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 13:30:40 2024 +0100
@@ -185,10 +185,10 @@
 
   /* zoom */
 
-  val zoom_component: GUI.Zoom =
+  val zoom_component: Font_Info.Zoom =
     new Font_Info.Zoom { override def changed(): Unit = zoom() }
 
-  def zoom(zoom: GUI.Zoom = zoom_component): Unit =
+  def zoom(zoom: Font_Info.Zoom = zoom_component): Unit =
     resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom))