1/* Title: Tools/jEdit/src/rich_text_area.scala 2 Author: Makarius 3 4Enhanced version of jEdit text area, with rich text rendering, 5tooltips, hyperlinks etc. 6*/ 7 8package isabelle.jedit 9 10 11import isabelle._ 12 13import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo} 14import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, 15 FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} 16import java.awt.font.TextAttribute 17import javax.swing.SwingUtilities 18import java.text.AttributedString 19import java.util.ArrayList 20 21import scala.util.matching.Regex 22 23import org.gjt.sp.util.Log 24import org.gjt.sp.jedit.{OperatingSystem, Debug, View} 25import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} 26import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea} 27 28 29class Rich_Text_Area( 30 view: View, 31 text_area: TextArea, 32 get_rendering: () => JEdit_Rendering, 33 close_action: () => Unit, 34 get_search_pattern: () => Option[Regex], 35 caret_update: () => Unit, 36 caret_visible: Boolean, 37 enable_hovering: Boolean) 38{ 39 private val buffer = text_area.getBuffer 40 41 42 /* robust extension body */ 43 44 def check_robust_body: Boolean = 45 GUI_Thread.require { buffer == text_area.getBuffer } 46 47 def robust_body[A](default: A)(body: => A): A = 48 { 49 try { 50 if (check_robust_body) body 51 else { 52 Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer")) 53 default 54 } 55 } 56 catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default } 57 } 58 59 60 /* original painters */ 61 62 private def pick_extension(name: String): TextAreaExtension = 63 { 64 text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList 65 match { 66 case List(x) => x 67 case _ => error("Expected exactly one " + name) 68 } 69 } 70 71 private val orig_text_painter = 72 pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") 73 74 75 /* common painter state */ 76 77 @volatile private var painter_rendering: JEdit_Rendering = null 78 @volatile private var painter_clip: Shape = null 79 @volatile private var caret_focus: Set[Long] = Set.empty 80 81 private val set_state = new TextAreaExtension 82 { 83 override def paintScreenLineRange(gfx: Graphics2D, 84 first_line: Int, last_line: Int, physical_lines: Array[Int], 85 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 86 { 87 painter_rendering = get_rendering() 88 painter_clip = gfx.getClip 89 caret_focus = 90 JEdit_Lib.visible_range(text_area) match { 91 case Some(visible_range) if caret_enabled && !painter_rendering.snapshot.is_outdated => 92 painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range) 93 case _ => Set.empty[Long] 94 } 95 } 96 } 97 98 private val reset_state = new TextAreaExtension 99 { 100 override def paintScreenLineRange(gfx: Graphics2D, 101 first_line: Int, last_line: Int, physical_lines: Array[Int], 102 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 103 { 104 painter_rendering = null 105 painter_clip = null 106 caret_focus = Set.empty 107 } 108 } 109 110 def robust_rendering(body: JEdit_Rendering => Unit) 111 { 112 robust_body(()) { body(painter_rendering) } 113 } 114 115 116 /* active areas within the text */ 117 118 private class Active_Area[A]( 119 rendering: JEdit_Rendering => Text.Range => Option[Text.Info[A]], 120 cursor: Option[Int]) 121 { 122 private var the_text_info: Option[(String, Text.Info[A])] = None 123 124 def is_active: Boolean = the_text_info.isDefined 125 def text_info: Option[(String, Text.Info[A])] = the_text_info 126 def info: Option[Text.Info[A]] = the_text_info.map(_._2) 127 128 def update(new_info: Option[Text.Info[A]]) 129 { 130 val old_text_info = the_text_info 131 val new_text_info = 132 new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) 133 134 if (new_text_info != old_text_info) { 135 caret_update() 136 if (cursor.isDefined) { 137 if (new_text_info.isDefined) 138 text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) 139 else 140 text_area.getPainter.resetCursor() 141 } 142 for { 143 r0 <- JEdit_Lib.visible_range(text_area) 144 opt <- List(old_text_info, new_text_info) 145 (_, Text.Info(r1, _)) <- opt 146 r2 <- r1.try_restrict(r0) // FIXME more precise?! 147 } JEdit_Lib.invalidate_range(text_area, r2) 148 the_text_info = new_text_info 149 } 150 } 151 152 def update_rendering(r: JEdit_Rendering, range: Text.Range) 153 { update(rendering(r)(range)) } 154 155 def reset { update(None) } 156 } 157 158 // owned by GUI thread 159 160 private val highlight_area = 161 new Active_Area[Color]( 162 (rendering: JEdit_Rendering) => rendering.highlight _, None) 163 164 private val hyperlink_area = 165 new Active_Area[PIDE.editor.Hyperlink]( 166 (rendering: JEdit_Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR)) 167 168 private val active_area = 169 new Active_Area[XML.Elem]( 170 (rendering: JEdit_Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR)) 171 172 private val active_areas = 173 List((highlight_area, true), (hyperlink_area, true), (active_area, false)) 174 def active_reset(): Unit = active_areas.foreach(_._1.reset) 175 176 private def area_active(): Boolean = 177 active_areas.exists({ case (area, _) => area.is_active }) 178 179 private val focus_listener = new FocusAdapter { 180 override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } } 181 } 182 183 private val window_listener = new WindowAdapter { 184 override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } } 185 override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } } 186 } 187 188 private val mouse_listener = new MouseAdapter { 189 override def mouseClicked(e: MouseEvent) { 190 robust_body(()) { 191 hyperlink_area.info match { 192 case Some(Text.Info(range, link)) => 193 if (!link.external) { 194 try { text_area.moveCaretPosition(range.start) } 195 catch { 196 case _: ArrayIndexOutOfBoundsException => 197 case _: IllegalArgumentException => 198 } 199 text_area.requestFocus 200 } 201 link.follow(view) 202 case None => 203 } 204 active_area.text_info match { 205 case Some((text, Text.Info(_, markup))) => 206 Active.action(view, text, markup) 207 close_action() 208 case None => 209 } 210 } 211 } 212 } 213 214 private def mouse_inside_painter(): Boolean = 215 MouseInfo.getPointerInfo match { 216 case null => false 217 case info => 218 val point = info.getLocation 219 val painter = text_area.getPainter 220 SwingUtilities.convertPointFromScreen(point, painter) 221 painter.contains(point) 222 } 223 224 private val mouse_motion_listener = new MouseMotionAdapter { 225 override def mouseDragged(evt: MouseEvent) { 226 robust_body(()) { 227 active_reset() 228 Completion_Popup.Text_Area.dismissed(text_area) 229 Pretty_Tooltip.dismiss_descendant(text_area.getPainter) 230 } 231 } 232 233 override def mouseMoved(evt: MouseEvent) { 234 robust_body(()) { 235 val x = evt.getX 236 val y = evt.getY 237 val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 238 239 if ((control || enable_hovering) && !buffer.isLoading) { 240 JEdit_Lib.buffer_lock(buffer) { 241 JEdit_Lib.pixel_range(text_area, x, y) match { 242 case None => active_reset() 243 case Some(range) => 244 val rendering = get_rendering() 245 for ((area, require_control) <- active_areas) 246 { 247 if (control == require_control && !rendering.snapshot.is_outdated) 248 area.update_rendering(rendering, range) 249 else area.reset 250 } 251 } 252 } 253 } 254 else active_reset() 255 256 if (evt.getSource == text_area.getPainter) { 257 Pretty_Tooltip.invoke(() => 258 robust_body(()) { 259 if (mouse_inside_painter()) { 260 val rendering = get_rendering() 261 val snapshot = rendering.snapshot 262 if (!snapshot.is_outdated) { 263 JEdit_Lib.pixel_range(text_area, x, y) match { 264 case None => 265 case Some(range) => 266 val result = 267 if (control) rendering.tooltip(range) 268 else rendering.tooltip_message(range) 269 result match { 270 case None => 271 case Some(tip) => 272 val painter = text_area.getPainter 273 val loc = new Point(x, y + painter.getLineHeight / 2) 274 val results = snapshot.command_results(tip.range) 275 Pretty_Tooltip(view, painter, loc, rendering, results, tip) 276 } 277 } 278 } 279 } 280 }) 281 } 282 } 283 } 284 } 285 286 287 /* text background */ 288 289 private val background_painter = new TextAreaExtension 290 { 291 override def paintScreenLineRange(gfx: Graphics2D, 292 first_line: Int, last_line: Int, physical_lines: Array[Int], 293 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 294 { 295 robust_rendering { rendering => 296 val fm = text_area.getPainter.getFontMetrics 297 298 for (i <- 0 until physical_lines.length) { 299 if (physical_lines(i) != -1) { 300 val line_range = Text.Range(start(i), end(i) min buffer.getLength) 301 302 // line background color 303 for { (c, separator) <- rendering.line_background(line_range) } 304 { 305 gfx.setColor(rendering.color(c)) 306 val sep = if (separator) 2 min (line_height / 2) else 0 307 gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) 308 } 309 310 // background color 311 for { 312 Text.Info(range, c) <- 313 rendering.background(Rendering.background_elements, line_range, caret_focus) 314 r <- JEdit_Lib.gfx_range(text_area, range) 315 } { 316 gfx.setColor(rendering.color(c)) 317 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 318 } 319 320 // active area -- potentially from other snapshot 321 for { 322 info <- active_area.info 323 Text.Info(range, _) <- info.try_restrict(line_range) 324 r <- JEdit_Lib.gfx_range(text_area, range) 325 } { 326 gfx.setColor(rendering.active_hover_color) 327 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 328 } 329 330 // squiggly underline 331 for { 332 Text.Info(range, c) <- rendering.squiggly_underline(line_range) 333 r <- JEdit_Lib.gfx_range(text_area, range) 334 } { 335 gfx.setColor(rendering.color(c)) 336 val x0 = (r.x / 2) * 2 337 val y0 = r.y + fm.getAscent + 1 338 for (x1 <- Range(x0, x0 + r.length, 2)) { 339 val y1 = if (x1 % 4 < 2) y0 else y0 + 1 340 gfx.drawLine(x1, y1, x1 + 1, y1) 341 } 342 } 343 344 // spell checker 345 for { 346 spell_checker <- PIDE.plugin.spell_checker.get 347 spell <- rendering.spell_checker(line_range) 348 text <- JEdit_Lib.get_text(buffer, spell.range) 349 info <- spell_checker.marked_words(spell.range.start, text) 350 r <- JEdit_Lib.gfx_range(text_area, info.range) 351 } { 352 gfx.setColor(rendering.spell_checker_color) 353 val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2)) 354 gfx.drawLine(r.x, y0, r.x + r.length, y0) 355 } 356 } 357 } 358 } 359 } 360 } 361 362 363 /* text */ 364 365 private def caret_enabled: Boolean = 366 caret_visible && (!text_area.hasFocus || text_area.isCaretVisible) 367 368 private def caret_color(rendering: JEdit_Rendering, offset: Text.Offset): Color = 369 { 370 if (text_area.isCaretVisible) text_area.getPainter.getCaretColor 371 else { 372 val debug_positions = 373 (for { 374 c <- PIDE.session.debugger.focus().iterator 375 pos <- c.debug_position.iterator 376 } yield pos).toList 377 if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _))) 378 rendering.caret_debugger_color 379 else rendering.caret_invisible_color 380 } 381 } 382 383 private def paint_chunk_list(rendering: JEdit_Rendering, 384 gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = 385 { 386 val clip_rect = gfx.getClipBounds 387 val painter = text_area.getPainter 388 val font_context = painter.getFontRenderContext 389 390 val caret_range = 391 if (caret_enabled) JEdit_Lib.caret_range(text_area) 392 else Text.Range.offside 393 394 var w = 0.0f 395 var chunk = head 396 while (chunk != null) { 397 val chunk_offset = line_start + chunk.offset 398 if (x + w + chunk.width > clip_rect.x && 399 x + w < clip_rect.x + clip_rect.width && chunk.length > 0) 400 { 401 val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length) 402 val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str 403 val chunk_font = chunk.style.getFont 404 val chunk_color = chunk.style.getForegroundColor 405 406 def string_width(s: String): Float = 407 if (s.isEmpty) 0.0f 408 else chunk_font.getStringBounds(s, font_context).getWidth.toFloat 409 410 val markup = 411 for { 412 r1 <- rendering.text_color(chunk_range, chunk_color) 413 r2 <- r1.try_restrict(chunk_range) 414 } yield r2 415 416 val padded_markup_iterator = 417 if (markup.isEmpty) 418 Iterator(Text.Info(chunk_range, chunk_color)) 419 else 420 Iterator( 421 Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++ 422 markup.iterator ++ 423 Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color)) 424 425 var x1 = x + w 426 gfx.setFont(chunk_font) 427 for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) { 428 val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset) 429 gfx.setColor(color) 430 431 range.try_restrict(caret_range) match { 432 case Some(r) if !r.is_singularity => 433 val i = r.start - range.start 434 val j = r.stop - range.start 435 val s1 = str.substring(0, i) 436 val s2 = str.substring(i, j) 437 val s3 = str.substring(j) 438 439 if (s1.nonEmpty) gfx.drawString(Word.bidi_override(s1), x1, y) 440 441 val astr = new AttributedString(Word.bidi_override(s2)) 442 astr.addAttribute(TextAttribute.FONT, chunk_font) 443 astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start)) 444 astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) 445 gfx.drawString(astr.getIterator, x1 + string_width(s1), y) 446 447 if (s3.nonEmpty) 448 gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y) 449 450 case _ => 451 gfx.drawString(Word.bidi_override(str), x1, y) 452 } 453 x1 += string_width(str) 454 } 455 } 456 w += chunk.width 457 chunk = chunk.next.asInstanceOf[Chunk] 458 } 459 w 460 } 461 462 private val text_painter = new TextAreaExtension 463 { 464 override def paintScreenLineRange(gfx: Graphics2D, 465 first_line: Int, last_line: Int, physical_lines: Array[Int], 466 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 467 { 468 robust_rendering { rendering => 469 val painter = text_area.getPainter 470 val fm = painter.getFontMetrics 471 val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext) 472 473 val clip = gfx.getClip 474 val x0 = text_area.getHorizontalOffset 475 var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent 476 477 val (bullet_x, bullet_y, bullet_w, bullet_h) = 478 { 479 val w = fm.charWidth(' ') 480 val b = (w / 2) max 1 481 val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt 482 ((w - b + 1) / 2, c - b / 2, w - b, line_height - b) 483 } 484 485 for (i <- 0 until physical_lines.length) { 486 val line = physical_lines(i) 487 if (line != -1) { 488 val line_range = Text.Range(start(i), end(i) min buffer.getLength) 489 490 // text chunks 491 val screen_line = first_line + i 492 val chunks = text_area.getChunksOfScreenLine(screen_line) 493 if (chunks != null) { 494 try { 495 val line_start = buffer.getLineStartOffset(line) 496 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) 497 val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt 498 gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) 499 orig_text_painter.paintValidLine(gfx, 500 screen_line, line, start(i), end(i), y + line_height * i) 501 } finally { gfx.setClip(clip) } 502 } 503 504 // bullet bar 505 for { 506 Text.Info(range, color) <- rendering.bullet(line_range) 507 r <- JEdit_Lib.gfx_range(text_area, range) 508 } { 509 gfx.setColor(color) 510 gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y, 511 r.length - bullet_w, line_height - bullet_h) 512 } 513 } 514 y0 += line_height 515 } 516 } 517 } 518 } 519 520 521 /* foreground */ 522 523 private val foreground_painter = new TextAreaExtension 524 { 525 override def paintScreenLineRange(gfx: Graphics2D, 526 first_line: Int, last_line: Int, physical_lines: Array[Int], 527 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 528 { 529 robust_rendering { rendering => 530 val search_pattern = get_search_pattern() 531 for (i <- 0 until physical_lines.length) { 532 if (physical_lines(i) != -1) { 533 val line_range = Text.Range(start(i), end(i) min buffer.getLength) 534 535 // foreground color 536 for { 537 Text.Info(range, c) <- rendering.foreground(line_range) 538 r <- JEdit_Lib.gfx_range(text_area, range) 539 } { 540 gfx.setColor(rendering.color(c)) 541 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 542 } 543 544 // search pattern 545 for { 546 regex <- search_pattern 547 text <- JEdit_Lib.get_text(buffer, line_range) 548 m <- regex.findAllMatchIn(text) 549 range = Text.Range(m.start, m.end) + line_range.start 550 r <- JEdit_Lib.gfx_range(text_area, range) 551 } { 552 gfx.setColor(rendering.search_color) 553 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 554 } 555 556 // highlight range -- potentially from other snapshot 557 for { 558 info <- highlight_area.info 559 Text.Info(range, color) <- info.try_restrict(line_range) 560 r <- JEdit_Lib.gfx_range(text_area, range) 561 } { 562 gfx.setColor(color) 563 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 564 } 565 566 // hyperlink range -- potentially from other snapshot 567 for { 568 info <- hyperlink_area.info 569 Text.Info(range, _) <- info.try_restrict(line_range) 570 r <- JEdit_Lib.gfx_range(text_area, range) 571 } { 572 gfx.setColor(rendering.hyperlink_color) 573 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) 574 } 575 576 // entity def range 577 if (!area_active() && caret_visible) { 578 for { 579 Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) 580 r <- JEdit_Lib.gfx_range(text_area, range) 581 } { 582 gfx.setColor(color) 583 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) 584 } 585 } 586 587 // completion range 588 if (!area_active() && caret_visible) { 589 for { 590 completion <- Completion_Popup.Text_Area(text_area) 591 Text.Info(range, color) <- completion.rendering(rendering, line_range) 592 r <- JEdit_Lib.gfx_range(text_area, range) 593 } { 594 gfx.setColor(color) 595 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) 596 } 597 } 598 } 599 } 600 } 601 } 602 } 603 604 605 /* caret -- outside of text range */ 606 607 private class Caret_Painter(before: Boolean) extends TextAreaExtension 608 { 609 override def paintValidLine(gfx: Graphics2D, 610 screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) 611 { 612 robust_rendering { _ => 613 if (before) gfx.clipRect(0, 0, 0, 0) 614 else gfx.setClip(painter_clip) 615 } 616 } 617 } 618 619 private val before_caret_painter1 = new Caret_Painter(true) 620 private val after_caret_painter1 = new Caret_Painter(false) 621 private val before_caret_painter2 = new Caret_Painter(true) 622 private val after_caret_painter2 = new Caret_Painter(false) 623 624 private val caret_painter = new TextAreaExtension 625 { 626 override def paintValidLine(gfx: Graphics2D, 627 screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) 628 { 629 robust_rendering { rendering => 630 if (caret_visible) { 631 val caret = text_area.getCaretPosition 632 if (caret_enabled && start <= caret && caret == end - 1) { 633 val painter = text_area.getPainter 634 val fm = painter.getFontMetrics 635 636 val offset = caret - text_area.getLineStartOffset(physical_line) 637 val x = text_area.offsetToXY(physical_line, offset).x 638 val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent 639 640 val astr = new AttributedString(" ") 641 astr.addAttribute(TextAttribute.FONT, painter.getFont) 642 astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret)) 643 astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) 644 645 val clip = gfx.getClip 646 try { 647 gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight) 648 gfx.drawString(astr.getIterator, x, y1) 649 } 650 finally { gfx.setClip(clip) } 651 } 652 } 653 } 654 } 655 } 656 657 658 /* activation */ 659 660 def activate() 661 { 662 val painter = text_area.getPainter 663 painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) 664 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) 665 painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) 666 painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) 667 painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) 668 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) 669 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2) 670 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) 671 painter.addExtension(500, foreground_painter) 672 painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state) 673 painter.removeExtension(orig_text_painter) 674 painter.addMouseListener(mouse_listener) 675 painter.addMouseMotionListener(mouse_motion_listener) 676 text_area.addFocusListener(focus_listener) 677 view.addWindowListener(window_listener) 678 } 679 680 def deactivate() 681 { 682 active_reset() 683 val painter = text_area.getPainter 684 view.removeWindowListener(window_listener) 685 text_area.removeFocusListener(focus_listener) 686 painter.removeMouseMotionListener(mouse_motion_listener) 687 painter.removeMouseListener(mouse_listener) 688 painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) 689 painter.removeExtension(reset_state) 690 painter.removeExtension(foreground_painter) 691 painter.removeExtension(caret_painter) 692 painter.removeExtension(after_caret_painter2) 693 painter.removeExtension(before_caret_painter2) 694 painter.removeExtension(after_caret_painter1) 695 painter.removeExtension(before_caret_painter1) 696 painter.removeExtension(text_painter) 697 painter.removeExtension(background_painter) 698 painter.removeExtension(set_state) 699 } 700} 701