author | wenzelm |
Wed, 21 May 2014 16:21:11 +0200 | |
changeset 57044 | 042d6e58cb40 |
parent 56662 | f373fb77e0a4 |
child 57612 | 990ffb84489b |
permissions | -rw-r--r-- |
55827 | 1 |
/* Title: Tools/jEdit/src/font_info.scala |
55825 | 2 |
Author: Makarius |
3 |
||
55827 | 4 |
Font information, derived from main jEdit view font. |
55825 | 5 |
*/ |
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
||
13 |
import java.awt.Font |
|
14 |
||
15 |
import org.gjt.sp.jedit.{jEdit, View} |
|
16 |
||
17 |
||
18 |
object Font_Info |
|
19 |
{ |
|
20 |
/* size range */ |
|
21 |
||
22 |
val min_size = 5 |
|
23 |
val max_size = 250 |
|
24 |
||
25 |
def restrict_size(size: Float): Float = size max min_size min max_size |
|
26 |
||
27 |
||
55827 | 28 |
/* main jEdit font */ |
55825 | 29 |
|
30 |
def main_family(): String = jEdit.getProperty("view.font") |
|
31 |
||
32 |
def main_size(scale: Double = 1.0): Float = |
|
33 |
restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat) |
|
34 |
||
35 |
def main(scale: Double = 1.0): Font_Info = |
|
36 |
Font_Info(main_family(), main_size(scale)) |
|
37 |
||
55827 | 38 |
|
39 |
/* incremental size change */ |
|
40 |
||
41 |
object main_change |
|
55825 | 42 |
{ |
55827 | 43 |
private def change_size(change: Float => Float) |
44 |
{ |
|
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
55827
diff
changeset
|
45 |
Swing_Thread.require {} |
55827 | 46 |
|
47 |
val size0 = main_size() |
|
48 |
val size = restrict_size(change(size0)).round |
|
49 |
if (size != size0) { |
|
50 |
jEdit.setIntegerProperty("view.fontsize", size) |
|
51 |
jEdit.propertiesChanged() |
|
52 |
jEdit.saveSettings() |
|
53 |
jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size) |
|
54 |
} |
|
55 |
} |
|
56 |
||
57 |
// owned by Swing thread |
|
58 |
private var steps = 0 |
|
59 |
private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) |
|
60 |
{ |
|
61 |
change_size(size => |
|
62 |
{ |
|
63 |
var i = size.round |
|
64 |
while (steps != 0 && i > 0) { |
|
65 |
if (steps > 0) |
|
66 |
{ i += (i / 10) max 1; steps -= 1 } |
|
67 |
else |
|
68 |
{ i -= (i / 10) max 1; steps += 1 } |
|
69 |
} |
|
70 |
steps = 0 |
|
71 |
i.toFloat |
|
72 |
}) |
|
73 |
} |
|
74 |
||
75 |
def step(i: Int) |
|
76 |
{ |
|
77 |
steps += i |
|
78 |
delay.invoke() |
|
79 |
} |
|
80 |
||
81 |
def reset(size: Float) |
|
82 |
{ |
|
83 |
delay.revoke() |
|
84 |
steps = 0 |
|
85 |
change_size(_ => size) |
|
55825 | 86 |
} |
87 |
} |
|
57044 | 88 |
|
89 |
||
90 |
/* zoom box */ |
|
91 |
||
92 |
abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" } |
|
55825 | 93 |
} |
94 |
||
95 |
sealed case class Font_Info(family: String, size: Float) |
|
96 |
{ |
|
97 |
def font: Font = new Font(family, Font.PLAIN, size.round) |
|
98 |
} |
|
99 |