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