equal
deleted
inserted
replaced
20 /* size range */ |
20 /* size range */ |
21 |
21 |
22 val min_size = 5 |
22 val min_size = 5 |
23 val max_size = 250 |
23 val max_size = 250 |
24 |
24 |
25 def restrict_size(size: Float): Float = size max min_size min max_size |
25 def restrict_size(size: Float): Float = size max min_size.toFloat min max_size.toFloat |
26 |
26 |
27 |
27 |
28 /* main jEdit font */ |
28 /* main jEdit font */ |
29 |
29 |
30 def main_family(): String = jEdit.getProperty("view.font") |
30 def main_family(): String = jEdit.getProperty("view.font") |