# HG changeset patch
# User wenzelm
# Date 1730977712 -3600
# Node ID 5e8287d34295dc022279c9485c937f64124cff19
# Parent  76f74ac9edee8035f3ea8817e2d1f42184ff0ef8
clarified signature;

diff -r 76f74ac9edee -r 5e8287d34295 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Nov 07 11:46:21 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Nov 07 12:08:32 2024 +0100
@@ -222,17 +222,18 @@
 
   /* zoom factor */
 
-  private val Zoom_Factor = "([0-9]+)%?".r
+  private val Percent = "([0-9]+)%?".r
 
   class Zoom extends Selector[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
       .map(GUI.Selector.item)
   ) {
-    def factor: Int = parse(selection.item.toString)
+    def percent: Int = parse(selection.item.toString)
+    def scale: Double = 0.01 * percent
 
     private def parse(text: String): Int =
       text match {
-        case Zoom_Factor(s) =>
+        case Percent(s) =>
           val i = Integer.parseInt(s)
           if (10 <= i && i < 1000) i else 100
         case _ => 100
diff -r 76f74ac9edee -r 5e8287d34295 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Thu Nov 07 11:46:21 2024 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Nov 07 12:08:32 2024 +0100
@@ -298,7 +298,7 @@
     tooltip = "Save current graph layout as PNG or PDF"
   }
 
-  private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(0.01 * factor) }
+  private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(scale) }
 
   private val fit_window = new Button {
     action = Action("Fit to window") { fit_to_window() }
diff -r 76f74ac9edee -r 5e8287d34295 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 11:46:21 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 12:08:32 2024 +0100
@@ -123,8 +123,8 @@
   }
 
   def zoom(zoom: GUI.Zoom): Unit = {
-    val factor = if (zoom == null) 100 else zoom.factor
-    resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale") * factor / 100))
+    val percent = if (zoom == null) 100 else zoom.percent
+    resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale") * percent / 100))
   }
 
   def update(
diff -r 76f74ac9edee -r 5e8287d34295 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Nov 07 11:46:21 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Nov 07 12:08:32 2024 +0100
@@ -63,7 +63,7 @@
 
   private def do_paint(): Unit = {
     GUI_Thread.later {
-      text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
+      text_area.resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale")))
     }
   }