equal
deleted
inserted
replaced
82 } |
82 } |
83 |
83 |
84 |
84 |
85 class Plugin extends EBPlugin |
85 class Plugin extends EBPlugin |
86 { |
86 { |
87 /* Isabelle font */ |
|
88 |
|
89 var font: Font = null |
|
90 val font_changed = new Event_Bus[Font] |
|
91 |
|
92 def set_font(size: Int) |
|
93 { |
|
94 font = Font.createFont(Font.TRUETYPE_FONT, |
|
95 Isabelle.system.platform_file("~~/lib/fonts/IsabelleMono.ttf")). |
|
96 deriveFont(Font.PLAIN, (size max 1).toFloat) |
|
97 font_changed.event(font) |
|
98 } |
|
99 |
|
100 |
|
101 /* event buses */ |
87 /* event buses */ |
102 |
88 |
103 val state_update = new Event_Bus[Command] |
89 val state_update = new Event_Bus[Command] |
104 |
90 |
105 |
91 |
152 } |
138 } |
153 } |
139 } |
154 |
140 |
155 override def start() |
141 override def start() |
156 { |
142 { |
|
143 Isabelle.plugin = this |
157 Isabelle.system = new Isabelle_System |
144 Isabelle.system = new Isabelle_System |
158 Isabelle.plugin = this |
145 if (!Isabelle.system.register_fonts()) |
159 set_font(Isabelle.Int_Property("font-size")) |
146 System.err.println("Failed to register Isabelle fonts") |
160 } |
147 } |
161 |
148 |
162 override def stop() |
149 override def stop() |
163 { |
150 { |
164 // TODO: proper cleanup |
151 // TODO: proper cleanup |