1/*  Title:      Tools/jEdit/src/font_info.scala
2    Author:     Makarius
3
4Font information, derived from main jEdit view font.
5*/
6
7package isabelle.jedit
8
9
10import isabelle._
11
12
13import java.awt.Font
14
15import org.gjt.sp.jedit.{jEdit, View}
16
17
18object 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
28  /* main jEdit font */
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
38
39  /* incremental size change */
40
41  object main_change
42  {
43    private def change_size(change: Float => Float)
44    {
45      GUI_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 GUI thread
58    private var steps = 0
59    private val delay = GUI_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)
86    }
87  }
88
89
90  /* zoom box */
91
92  abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" }
93}
94
95sealed case class Font_Info(family: String, size: Float)
96{
97  def font: Font = new Font(family, Font.PLAIN, size.round)
98}
99
100