changeset 81382 | 5e8287d34295 |
parent 81335 | fe32eaea366c |
child 81648 | c98cfdcb2df0 |
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 |