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 |
{
|
|
45 |
Swing_Thread.require()
|
|
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 |
}
|
|
88 |
}
|
|
89 |
|
|
90 |
sealed case class Font_Info(family: String, size: Float)
|
|
91 |
{
|
|
92 |
def font: Font = new Font(family, Font.PLAIN, size.round)
|
|
93 |
}
|
|
94 |
|