1 /* Title: Tools/jEdit/src/jedit/document_view.scala |
|
2 Author: Fabian Immler, TU Munich |
|
3 Author: Makarius |
|
4 |
|
5 Document view connected to jEdit text area. |
|
6 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 |
|
11 import isabelle._ |
|
12 |
|
13 import scala.actors.Actor._ |
|
14 |
|
15 import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point} |
|
16 import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, |
|
17 FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} |
|
18 import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory} |
|
19 import javax.swing.event.{CaretListener, CaretEvent} |
|
20 import java.util.ArrayList |
|
21 |
|
22 import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug} |
|
23 import org.gjt.sp.jedit.gui.RolloverButton |
|
24 import org.gjt.sp.jedit.options.GutterOptionPane |
|
25 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter} |
|
26 import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token} |
|
27 |
|
28 |
|
29 object Document_View |
|
30 { |
|
31 /* document view of text area */ |
|
32 |
|
33 private val key = new Object |
|
34 |
|
35 def init(model: Document_Model, text_area: JEditTextArea): Document_View = |
|
36 { |
|
37 Swing_Thread.require() |
|
38 val doc_view = new Document_View(model, text_area) |
|
39 text_area.putClientProperty(key, doc_view) |
|
40 doc_view.activate() |
|
41 doc_view |
|
42 } |
|
43 |
|
44 def apply(text_area: JEditTextArea): Option[Document_View] = |
|
45 { |
|
46 Swing_Thread.require() |
|
47 text_area.getClientProperty(key) match { |
|
48 case doc_view: Document_View => Some(doc_view) |
|
49 case _ => None |
|
50 } |
|
51 } |
|
52 |
|
53 def exit(text_area: JEditTextArea) |
|
54 { |
|
55 Swing_Thread.require() |
|
56 apply(text_area) match { |
|
57 case None => |
|
58 case Some(doc_view) => |
|
59 doc_view.deactivate() |
|
60 text_area.putClientProperty(key, null) |
|
61 } |
|
62 } |
|
63 } |
|
64 |
|
65 |
|
66 class Document_View(val model: Document_Model, text_area: JEditTextArea) |
|
67 { |
|
68 private val session = model.session |
|
69 |
|
70 |
|
71 /** token handling **/ |
|
72 |
|
73 /* extended token styles */ |
|
74 |
|
75 private var styles: Array[SyntaxStyle] = null // owned by Swing thread |
|
76 |
|
77 def extend_styles() |
|
78 { |
|
79 Swing_Thread.require() |
|
80 styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles) |
|
81 } |
|
82 extend_styles() |
|
83 |
|
84 def set_styles() |
|
85 { |
|
86 Swing_Thread.require() |
|
87 text_area.getPainter.setStyles(styles) |
|
88 } |
|
89 |
|
90 |
|
91 /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */ |
|
92 |
|
93 def wrap_margin(): Int = |
|
94 { |
|
95 val buffer = text_area.getBuffer |
|
96 val painter = text_area.getPainter |
|
97 val font = painter.getFont |
|
98 val font_context = painter.getFontRenderContext |
|
99 |
|
100 val soft_wrap = buffer.getStringProperty("wrap") == "soft" |
|
101 val max = buffer.getIntegerProperty("maxLineLen", 0) |
|
102 |
|
103 if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt |
|
104 else if (soft_wrap) |
|
105 painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3 |
|
106 else 0 |
|
107 } |
|
108 |
|
109 |
|
110 /* chunks */ |
|
111 |
|
112 def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] = |
|
113 { |
|
114 import scala.collection.JavaConversions._ |
|
115 |
|
116 val buffer = text_area.getBuffer |
|
117 val painter = text_area.getPainter |
|
118 val margin = wrap_margin().toFloat |
|
119 |
|
120 val out = new ArrayList[Chunk] |
|
121 val handler = new DisplayTokenHandler |
|
122 |
|
123 var result = Map[Text.Offset, Chunk]() |
|
124 for (line <- physical_lines) { |
|
125 out.clear |
|
126 handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin) |
|
127 buffer.markTokens(line, handler) |
|
128 |
|
129 val line_start = buffer.getLineStartOffset(line) |
|
130 for (chunk <- handler.getChunkList.iterator) |
|
131 result += (line_start + chunk.offset -> chunk) |
|
132 } |
|
133 result |
|
134 } |
|
135 |
|
136 |
|
137 /* visible line ranges */ |
|
138 |
|
139 // simplify slightly odd result of TextArea.getScreenLineEndOffset etc. |
|
140 // NB: jEdit already normalizes \r\n and \r to \n |
|
141 def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range = |
|
142 { |
|
143 val stop = if (start < end) end - 1 else end min model.buffer.getLength |
|
144 Text.Range(start, stop) |
|
145 } |
|
146 |
|
147 def screen_lines_range(): Text.Range = |
|
148 { |
|
149 val start = text_area.getScreenLineStartOffset(0) |
|
150 val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0) |
|
151 proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength) |
|
152 } |
|
153 |
|
154 def invalidate_line_range(range: Text.Range) |
|
155 { |
|
156 text_area.invalidateLineRange( |
|
157 model.buffer.getLineOfOffset(range.start), |
|
158 model.buffer.getLineOfOffset(range.stop)) |
|
159 } |
|
160 |
|
161 |
|
162 /* HTML popups */ |
|
163 |
|
164 private var html_popup: Option[Popup] = None |
|
165 |
|
166 private def exit_popup() { html_popup.map(_.hide) } |
|
167 |
|
168 private val html_panel = |
|
169 new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) |
|
170 html_panel.setBorder(BorderFactory.createLineBorder(Color.black)) |
|
171 |
|
172 private def html_panel_resize() |
|
173 { |
|
174 Swing_Thread.now { |
|
175 html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) |
|
176 } |
|
177 } |
|
178 |
|
179 private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int) |
|
180 { |
|
181 exit_popup() |
|
182 /* FIXME broken |
|
183 val offset = text_area.xyToOffset(x, y) |
|
184 val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter) |
|
185 |
|
186 // FIXME snapshot.cumulate |
|
187 snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match { |
|
188 case Text.Info(_, Some(msg)) #:: _ => |
|
189 val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60) |
|
190 html_panel.render_sync(List(msg)) |
|
191 Thread.sleep(10) // FIXME !? |
|
192 popup.show |
|
193 html_popup = Some(popup) |
|
194 case _ => |
|
195 } |
|
196 */ |
|
197 } |
|
198 |
|
199 |
|
200 /* subexpression highlighting */ |
|
201 |
|
202 private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int) |
|
203 : Option[(Text.Range, Color)] = |
|
204 { |
|
205 val offset = text_area.xyToOffset(x, y) |
|
206 snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match { |
|
207 case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color)) |
|
208 case _ => None |
|
209 } |
|
210 } |
|
211 |
|
212 private var highlight_range: Option[(Text.Range, Color)] = None |
|
213 |
|
214 |
|
215 /* CONTROL-mouse management */ |
|
216 |
|
217 private var control: Boolean = false |
|
218 |
|
219 private def exit_control() |
|
220 { |
|
221 exit_popup() |
|
222 highlight_range = None |
|
223 } |
|
224 |
|
225 private val focus_listener = new FocusAdapter { |
|
226 override def focusLost(e: FocusEvent) { |
|
227 highlight_range = None // FIXME exit_control !? |
|
228 } |
|
229 } |
|
230 |
|
231 private val window_listener = new WindowAdapter { |
|
232 override def windowIconified(e: WindowEvent) { exit_control() } |
|
233 override def windowDeactivated(e: WindowEvent) { exit_control() } |
|
234 } |
|
235 |
|
236 private val mouse_motion_listener = new MouseMotionAdapter { |
|
237 override def mouseMoved(e: MouseEvent) { |
|
238 control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown |
|
239 val x = e.getX() |
|
240 val y = e.getY() |
|
241 |
|
242 if (!model.buffer.isLoaded) exit_control() |
|
243 else |
|
244 Isabelle.swing_buffer_lock(model.buffer) { |
|
245 val snapshot = model.snapshot |
|
246 |
|
247 if (control) init_popup(snapshot, x, y) |
|
248 |
|
249 highlight_range map { case (range, _) => invalidate_line_range(range) } |
|
250 highlight_range = if (control) subexp_range(snapshot, x, y) else None |
|
251 highlight_range map { case (range, _) => invalidate_line_range(range) } |
|
252 } |
|
253 } |
|
254 } |
|
255 |
|
256 |
|
257 /* TextArea painters */ |
|
258 |
|
259 private val background_painter = new TextAreaExtension |
|
260 { |
|
261 override def paintScreenLineRange(gfx: Graphics2D, |
|
262 first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
263 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
264 { |
|
265 Isabelle.swing_buffer_lock(model.buffer) { |
|
266 val snapshot = model.snapshot() |
|
267 val ascent = text_area.getPainter.getFontMetrics.getAscent |
|
268 |
|
269 for (i <- 0 until physical_lines.length) { |
|
270 if (physical_lines(i) != -1) { |
|
271 val line_range = proper_line_range(start(i), end(i)) |
|
272 |
|
273 // background color: status |
|
274 val cmds = snapshot.node.command_range(snapshot.revert(line_range)) |
|
275 for { |
|
276 (command, command_start) <- cmds if !command.is_ignored |
|
277 val range = line_range.restrict(snapshot.convert(command.range + command_start)) |
|
278 r <- Isabelle.gfx_range(text_area, range) |
|
279 color <- Isabelle_Markup.status_color(snapshot, command) |
|
280 } { |
|
281 gfx.setColor(color) |
|
282 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
283 } |
|
284 |
|
285 // background color (1): markup |
|
286 for { |
|
287 Text.Info(range, Some(color)) <- |
|
288 snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator |
|
289 r <- Isabelle.gfx_range(text_area, range) |
|
290 } { |
|
291 gfx.setColor(color) |
|
292 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) |
|
293 } |
|
294 |
|
295 // background color (2): markup |
|
296 for { |
|
297 Text.Info(range, Some(color)) <- |
|
298 snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator |
|
299 r <- Isabelle.gfx_range(text_area, range) |
|
300 } { |
|
301 gfx.setColor(color) |
|
302 gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4) |
|
303 } |
|
304 |
|
305 // sub-expression highlighting -- potentially from other snapshot |
|
306 highlight_range match { |
|
307 case Some((range, color)) if line_range.overlaps(range) => |
|
308 Isabelle.gfx_range(text_area, line_range.restrict(range)) match { |
|
309 case None => |
|
310 case Some(r) => |
|
311 gfx.setColor(color) |
|
312 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) |
|
313 } |
|
314 case _ => |
|
315 } |
|
316 |
|
317 // squiggly underline |
|
318 for { |
|
319 Text.Info(range, Some(color)) <- |
|
320 snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator |
|
321 r <- Isabelle.gfx_range(text_area, range) |
|
322 } { |
|
323 gfx.setColor(color) |
|
324 val x0 = (r.x / 2) * 2 |
|
325 val y0 = r.y + ascent + 1 |
|
326 for (x1 <- Range(x0, x0 + r.length, 2)) { |
|
327 val y1 = if (x1 % 4 < 2) y0 else y0 + 1 |
|
328 gfx.drawLine(x1, y1, x1 + 1, y1) |
|
329 } |
|
330 } |
|
331 } |
|
332 } |
|
333 } |
|
334 } |
|
335 |
|
336 override def getToolTipText(x: Int, y: Int): String = |
|
337 { |
|
338 Isabelle.swing_buffer_lock(model.buffer) { |
|
339 val snapshot = model.snapshot() |
|
340 val offset = text_area.xyToOffset(x, y) |
|
341 if (control) { |
|
342 snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match |
|
343 { |
|
344 case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text) |
|
345 case _ => null |
|
346 } |
|
347 } |
|
348 else { |
|
349 // FIXME snapshot.cumulate |
|
350 snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match |
|
351 { |
|
352 case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text) |
|
353 case _ => null |
|
354 } |
|
355 } |
|
356 } |
|
357 } |
|
358 } |
|
359 |
|
360 var use_text_painter = false |
|
361 |
|
362 private val text_painter = new TextAreaExtension |
|
363 { |
|
364 override def paintScreenLineRange(gfx: Graphics2D, |
|
365 first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
366 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
367 { |
|
368 if (use_text_painter) { |
|
369 Isabelle.swing_buffer_lock(model.buffer) { |
|
370 val painter = text_area.getPainter |
|
371 val fm = painter.getFontMetrics |
|
372 |
|
373 val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1)) |
|
374 |
|
375 val x0 = text_area.getHorizontalOffset |
|
376 var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent |
|
377 for (i <- 0 until physical_lines.length) { |
|
378 if (physical_lines(i) != -1) { |
|
379 all_chunks.get(start(i)) match { |
|
380 case Some(chunk) => |
|
381 Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR) |
|
382 case None => |
|
383 } |
|
384 } |
|
385 y0 += line_height |
|
386 } |
|
387 } |
|
388 } |
|
389 } |
|
390 } |
|
391 |
|
392 private val gutter_painter = new TextAreaExtension |
|
393 { |
|
394 override def paintScreenLineRange(gfx: Graphics2D, |
|
395 first_line: Int, last_line: Int, physical_lines: Array[Int], |
|
396 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
|
397 { |
|
398 val gutter = text_area.getGutter |
|
399 val width = GutterOptionPane.getSelectionAreaWidth |
|
400 val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3) |
|
401 val FOLD_MARKER_SIZE = 12 |
|
402 |
|
403 if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) { |
|
404 Isabelle.swing_buffer_lock(model.buffer) { |
|
405 val snapshot = model.snapshot() |
|
406 for (i <- 0 until physical_lines.length) { |
|
407 if (physical_lines(i) != -1) { |
|
408 val line_range = proper_line_range(start(i), end(i)) |
|
409 |
|
410 // gutter icons |
|
411 val icons = |
|
412 (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate |
|
413 snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator) |
|
414 yield icon).toList.sortWith(_ >= _) |
|
415 icons match { |
|
416 case icon :: _ => |
|
417 val icn = icon.icon |
|
418 val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10 |
|
419 val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0) |
|
420 icn.paintIcon(gutter, gfx, x0, y0) |
|
421 case Nil => |
|
422 } |
|
423 } |
|
424 } |
|
425 } |
|
426 } |
|
427 } |
|
428 } |
|
429 |
|
430 |
|
431 /* caret handling */ |
|
432 |
|
433 def selected_command(): Option[Command] = |
|
434 { |
|
435 Swing_Thread.require() |
|
436 model.snapshot().node.proper_command_at(text_area.getCaretPosition) |
|
437 } |
|
438 |
|
439 private val caret_listener = new CaretListener { |
|
440 private val delay = Swing_Thread.delay_last(session.input_delay) { |
|
441 session.perspective.event(Session.Perspective) |
|
442 } |
|
443 override def caretUpdate(e: CaretEvent) { delay() } |
|
444 } |
|
445 |
|
446 |
|
447 /* overview of command status left of scrollbar */ |
|
448 |
|
449 private val overview = new JPanel(new BorderLayout) |
|
450 { |
|
451 private val WIDTH = 10 |
|
452 private val HEIGHT = 2 |
|
453 |
|
454 setPreferredSize(new Dimension(WIDTH, 0)) |
|
455 |
|
456 setRequestFocusEnabled(false) |
|
457 |
|
458 addMouseListener(new MouseAdapter { |
|
459 override def mousePressed(event: MouseEvent) { |
|
460 val line = y_to_line(event.getY) |
|
461 if (line >= 0 && line < text_area.getLineCount) |
|
462 text_area.setCaretPosition(text_area.getLineStartOffset(line)) |
|
463 } |
|
464 }) |
|
465 |
|
466 override def addNotify() { |
|
467 super.addNotify() |
|
468 ToolTipManager.sharedInstance.registerComponent(this) |
|
469 } |
|
470 |
|
471 override def removeNotify() { |
|
472 ToolTipManager.sharedInstance.unregisterComponent(this) |
|
473 super.removeNotify |
|
474 } |
|
475 |
|
476 override def paintComponent(gfx: Graphics) |
|
477 { |
|
478 super.paintComponent(gfx) |
|
479 Swing_Thread.assert() |
|
480 |
|
481 val buffer = model.buffer |
|
482 Isabelle.buffer_lock(buffer) { |
|
483 val snapshot = model.snapshot() |
|
484 |
|
485 def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] = |
|
486 { |
|
487 try { |
|
488 val line1 = buffer.getLineOfOffset(snapshot.convert(start)) |
|
489 val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1 |
|
490 Some((line1, line2)) |
|
491 } |
|
492 catch { case e: ArrayIndexOutOfBoundsException => None } |
|
493 } |
|
494 for { |
|
495 (command, start) <- snapshot.node.command_starts |
|
496 if !command.is_ignored |
|
497 (line1, line2) <- line_range(command, start) |
|
498 val y = line_to_y(line1) |
|
499 val height = HEIGHT * (line2 - line1) |
|
500 color <- Isabelle_Markup.overview_color(snapshot, command) |
|
501 } { |
|
502 gfx.setColor(color) |
|
503 gfx.fillRect(0, y, getWidth - 1, height) |
|
504 } |
|
505 } |
|
506 } |
|
507 |
|
508 private def line_to_y(line: Int): Int = |
|
509 (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) |
|
510 |
|
511 private def y_to_line(y: Int): Int = |
|
512 (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight |
|
513 } |
|
514 |
|
515 |
|
516 /* main actor */ |
|
517 |
|
518 private val main_actor = actor { |
|
519 loop { |
|
520 react { |
|
521 case Session.Commands_Changed(changed) => |
|
522 val buffer = model.buffer |
|
523 Isabelle.swing_buffer_lock(buffer) { |
|
524 val snapshot = model.snapshot() |
|
525 |
|
526 if (changed.exists(snapshot.node.commands.contains)) |
|
527 overview.repaint() |
|
528 |
|
529 val visible_range = screen_lines_range() |
|
530 val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1) |
|
531 if (visible_cmds.exists(changed)) { |
|
532 for { |
|
533 line <- 0 until text_area.getVisibleLines |
|
534 val start = text_area.getScreenLineStartOffset(line) if start >= 0 |
|
535 val end = text_area.getScreenLineEndOffset(line) if end >= 0 |
|
536 val range = proper_line_range(start, end) |
|
537 val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) |
|
538 if line_cmds.exists(changed) |
|
539 } text_area.invalidateScreenLineRange(line, line) |
|
540 |
|
541 // FIXME danger of deadlock!? |
|
542 // FIXME potentially slow!? |
|
543 model.buffer.propertiesChanged() |
|
544 } |
|
545 } |
|
546 |
|
547 case Session.Global_Settings => html_panel_resize() |
|
548 |
|
549 case bad => System.err.println("command_change_actor: ignoring bad message " + bad) |
|
550 } |
|
551 } |
|
552 } |
|
553 |
|
554 |
|
555 /* activation */ |
|
556 |
|
557 private def activate() |
|
558 { |
|
559 val painter = text_area.getPainter |
|
560 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) |
|
561 painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter) |
|
562 text_area.getGutter.addExtension(gutter_painter) |
|
563 text_area.addFocusListener(focus_listener) |
|
564 text_area.getView.addWindowListener(window_listener) |
|
565 painter.addMouseMotionListener(mouse_motion_listener) |
|
566 text_area.addCaretListener(caret_listener) |
|
567 text_area.addLeftOfScrollBar(overview) |
|
568 session.commands_changed += main_actor |
|
569 session.global_settings += main_actor |
|
570 } |
|
571 |
|
572 private def deactivate() |
|
573 { |
|
574 val painter = text_area.getPainter |
|
575 session.commands_changed -= main_actor |
|
576 session.global_settings -= main_actor |
|
577 text_area.removeFocusListener(focus_listener) |
|
578 text_area.getView.removeWindowListener(window_listener) |
|
579 painter.removeMouseMotionListener(mouse_motion_listener) |
|
580 text_area.removeCaretListener(caret_listener) |
|
581 text_area.removeLeftOfScrollBar(overview) |
|
582 text_area.getGutter.removeExtension(gutter_painter) |
|
583 painter.removeExtension(text_painter) |
|
584 painter.removeExtension(background_painter) |
|
585 exit_popup() |
|
586 } |
|
587 } |
|