55825
|
1 |
/* Title: Tools/jEdit/src/jedit_font.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Font information, derived from main view font.
|
|
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 |
val dummy: Font_Info = Font_Info("Dialog", 12.0f)
|
|
21 |
|
|
22 |
|
|
23 |
/* size range */
|
|
24 |
|
|
25 |
val min_size = 5
|
|
26 |
val max_size = 250
|
|
27 |
|
|
28 |
def restrict_size(size: Float): Float = size max min_size min max_size
|
|
29 |
|
|
30 |
|
|
31 |
/* jEdit font */
|
|
32 |
|
|
33 |
def main_family(): String = jEdit.getProperty("view.font")
|
|
34 |
|
|
35 |
def main_size(scale: Double = 1.0): Float =
|
|
36 |
restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
|
|
37 |
|
|
38 |
def main(scale: Double = 1.0): Font_Info =
|
|
39 |
Font_Info(main_family(), main_size(scale))
|
|
40 |
|
|
41 |
def main_change(change: Float => Float)
|
|
42 |
{
|
|
43 |
val size0 = main_size()
|
|
44 |
val size = restrict_size(change(size0)).round
|
|
45 |
if (size != size0) {
|
|
46 |
jEdit.setIntegerProperty("view.fontsize", size)
|
|
47 |
jEdit.propertiesChanged()
|
|
48 |
jEdit.saveSettings()
|
|
49 |
jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
|
|
50 |
}
|
|
51 |
}
|
|
52 |
}
|
|
53 |
|
|
54 |
sealed case class Font_Info(family: String, size: Float)
|
|
55 |
{
|
|
56 |
def font: Font = new Font(family, Font.PLAIN, size.round)
|
|
57 |
}
|
|
58 |
|