src/Pure/GUI/gui.scala
changeset 81382 5e8287d34295
parent 81335 fe32eaea366c
child 81648 c98cfdcb2df0
equal deleted inserted replaced
81381:76f74ac9edee 81382:5e8287d34295
   220   }
   220   }
   221 
   221 
   222 
   222 
   223   /* zoom factor */
   223   /* zoom factor */
   224 
   224 
   225   private val Zoom_Factor = "([0-9]+)%?".r
   225   private val Percent = "([0-9]+)%?".r
   226 
   226 
   227   class Zoom extends Selector[String](
   227   class Zoom extends Selector[String](
   228     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
   228     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
   229       .map(GUI.Selector.item)
   229       .map(GUI.Selector.item)
   230   ) {
   230   ) {
   231     def factor: Int = parse(selection.item.toString)
   231     def percent: Int = parse(selection.item.toString)
       
   232     def scale: Double = 0.01 * percent
   232 
   233 
   233     private def parse(text: String): Int =
   234     private def parse(text: String): Int =
   234       text match {
   235       text match {
   235         case Zoom_Factor(s) =>
   236         case Percent(s) =>
   236           val i = Integer.parseInt(s)
   237           val i = Integer.parseInt(s)
   237           if (10 <= i && i < 1000) i else 100
   238           if (10 <= i && i < 1000) i else 100
   238         case _ => 100
   239         case _ => 100
   239       }
   240       }
   240 
   241