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 rendering.tooltip(range, control) match { 267 case None => 268 case Some(tip) => 269 val painter = text_area.getPainter 270 val loc = new Point(x, y + painter.getLineHeight / 2) 271 val results = snapshot.command_results(tip.range) 272 Pretty_Tooltip(view, painter, loc, rendering, results, tip) 273 } 274 } 275 } 276 } 277 }) 278 } 279 } 280 } 281 } 282 283 284 /* text background */ 285 286 private val background_painter = new TextAreaExtension 287 { 288 override def paintScreenLineRange(gfx: Graphics2D, 289 first_line: Int, last_line: Int, physical_lines: Array[Int], 290 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 291 { 292 robust_rendering { rendering => 293 val fm = text_area.getPainter.getFontMetrics 294 295 for (i <- 0 until physical_lines.length) { 296 if (physical_lines(i) != -1) { 297 val line_range = Text.Range(start(i), end(i) min buffer.getLength) 298 299 // line background color 300 for { (c, separator) <- rendering.line_background(line_range) } 301 { 302 gfx.setColor(rendering.color(c)) 303 val sep = if (separator) 2 min (line_height / 2) else 0 304 gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) 305 } 306 307 // background color 308 for { 309 Text.Info(range, c) <- 310 rendering.background(Rendering.background_elements, line_range, caret_focus) 311 r <- JEdit_Lib.gfx_range(text_area, range) 312 } { 313 gfx.setColor(rendering.color(c)) 314 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 315 } 316 317 // active area -- potentially from other snapshot 318 for { 319 info <- active_area.info 320 Text.Info(range, _) <- info.try_restrict(line_range) 321 r <- JEdit_Lib.gfx_range(text_area, range) 322 } { 323 gfx.setColor(rendering.active_hover_color) 324 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 325 } 326 327 // squiggly underline 328 for { 329 Text.Info(range, c) <- rendering.squiggly_underline(line_range) 330 r <- JEdit_Lib.gfx_range(text_area, range) 331 } { 332 gfx.setColor(rendering.color(c)) 333 val x0 = (r.x / 2) * 2 334 val y0 = r.y + fm.getAscent + 1 335 for (x1 <- Range(x0, x0 + r.length, 2)) { 336 val y1 = if (x1 % 4 < 2) y0 else y0 + 1 337 gfx.drawLine(x1, y1, x1 + 1, y1) 338 } 339 } 340 341 // spell checker 342 for { 343 spell_checker <- PIDE.plugin.spell_checker.get 344 spell <- rendering.spell_checker(line_range) 345 text <- JEdit_Lib.get_text(buffer, spell.range) 346 info <- spell_checker.marked_words(spell.range.start, text) 347 r <- JEdit_Lib.gfx_range(text_area, info.range) 348 } { 349 gfx.setColor(rendering.spell_checker_color) 350 val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2)) 351 gfx.drawLine(r.x, y0, r.x + r.length, y0) 352 } 353 } 354 } 355 } 356 } 357 } 358 359 360 /* text */ 361 362 private def caret_enabled: Boolean = 363 caret_visible && (!text_area.hasFocus || text_area.isCaretVisible) 364 365 private def caret_color(rendering: JEdit_Rendering, offset: Text.Offset): Color = 366 { 367 if (text_area.isCaretVisible) text_area.getPainter.getCaretColor 368 else { 369 val debug_positions = 370 (for { 371 c <- PIDE.session.debugger.focus().iterator 372 pos <- c.debug_position.iterator 373 } yield pos).toList 374 if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _))) 375 rendering.caret_debugger_color 376 else rendering.caret_invisible_color 377 } 378 } 379 380 private def paint_chunk_list(rendering: JEdit_Rendering, 381 gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = 382 { 383 val clip_rect = gfx.getClipBounds 384 val painter = text_area.getPainter 385 val font_context = painter.getFontRenderContext 386 387 val caret_range = 388 if (caret_enabled) JEdit_Lib.caret_range(text_area) 389 else Text.Range.offside 390 391 var w = 0.0f 392 var chunk = head 393 while (chunk != null) { 394 val chunk_offset = line_start + chunk.offset 395 if (x + w + chunk.width > clip_rect.x && 396 x + w < clip_rect.x + clip_rect.width && chunk.length > 0) 397 { 398 val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length) 399 val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str 400 val chunk_font = chunk.style.getFont 401 val chunk_color = chunk.style.getForegroundColor 402 403 def string_width(s: String): Float = 404 if (s.isEmpty) 0.0f 405 else chunk_font.getStringBounds(s, font_context).getWidth.toFloat 406 407 val markup = 408 for { 409 r1 <- rendering.text_color(chunk_range, chunk_color) 410 r2 <- r1.try_restrict(chunk_range) 411 } yield r2 412 413 val padded_markup_iterator = 414 if (markup.isEmpty) 415 Iterator(Text.Info(chunk_range, chunk_color)) 416 else 417 Iterator( 418 Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++ 419 markup.iterator ++ 420 Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color)) 421 422 var x1 = x + w 423 gfx.setFont(chunk_font) 424 for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) { 425 val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset) 426 gfx.setColor(color) 427 428 range.try_restrict(caret_range) match { 429 case Some(r) if !r.is_singularity => 430 val i = r.start - range.start 431 val j = r.stop - range.start 432 val s1 = str.substring(0, i) 433 val s2 = str.substring(i, j) 434 val s3 = str.substring(j) 435 436 if (s1.nonEmpty) gfx.drawString(Word.bidi_override(s1), x1, y) 437 438 val astr = new AttributedString(Word.bidi_override(s2)) 439 astr.addAttribute(TextAttribute.FONT, chunk_font) 440 astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start)) 441 astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) 442 gfx.drawString(astr.getIterator, x1 + string_width(s1), y) 443 444 if (s3.nonEmpty) 445 gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y) 446 447 case _ => 448 gfx.drawString(Word.bidi_override(str), x1, y) 449 } 450 x1 += string_width(str) 451 } 452 } 453 w += chunk.width 454 chunk = chunk.next.asInstanceOf[Chunk] 455 } 456 w 457 } 458 459 private val text_painter = new TextAreaExtension 460 { 461 override def paintScreenLineRange(gfx: Graphics2D, 462 first_line: Int, last_line: Int, physical_lines: Array[Int], 463 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 464 { 465 robust_rendering { rendering => 466 val painter = text_area.getPainter 467 val fm = painter.getFontMetrics 468 val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext) 469 470 val clip = gfx.getClip 471 val x0 = text_area.getHorizontalOffset 472 var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent 473 474 val (bullet_x, bullet_y, bullet_w, bullet_h) = 475 { 476 val w = fm.charWidth(' ') 477 val b = (w / 2) max 1 478 val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt 479 ((w - b + 1) / 2, c - b / 2, w - b, line_height - b) 480 } 481 482 for (i <- 0 until physical_lines.length) { 483 val line = physical_lines(i) 484 if (line != -1) { 485 val line_range = Text.Range(start(i), end(i) min buffer.getLength) 486 487 // text chunks 488 val screen_line = first_line + i 489 val chunks = text_area.getChunksOfScreenLine(screen_line) 490 if (chunks != null) { 491 try { 492 val line_start = buffer.getLineStartOffset(line) 493 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) 494 val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt 495 gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) 496 orig_text_painter.paintValidLine(gfx, 497 screen_line, line, start(i), end(i), y + line_height * i) 498 } finally { gfx.setClip(clip) } 499 } 500 501 // bullet bar 502 for { 503 Text.Info(range, color) <- rendering.bullet(line_range) 504 r <- JEdit_Lib.gfx_range(text_area, range) 505 } { 506 gfx.setColor(color) 507 gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y, 508 r.length - bullet_w, line_height - bullet_h) 509 } 510 } 511 y0 += line_height 512 } 513 } 514 } 515 } 516 517 518 /* foreground */ 519 520 private val foreground_painter = new TextAreaExtension 521 { 522 override def paintScreenLineRange(gfx: Graphics2D, 523 first_line: Int, last_line: Int, physical_lines: Array[Int], 524 start: Array[Int], end: Array[Int], y: Int, line_height: Int) 525 { 526 robust_rendering { rendering => 527 val search_pattern = get_search_pattern() 528 for (i <- 0 until physical_lines.length) { 529 if (physical_lines(i) != -1) { 530 val line_range = Text.Range(start(i), end(i) min buffer.getLength) 531 532 // foreground color 533 for { 534 Text.Info(range, c) <- rendering.foreground(line_range) 535 r <- JEdit_Lib.gfx_range(text_area, range) 536 } { 537 gfx.setColor(rendering.color(c)) 538 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 539 } 540 541 // search pattern 542 for { 543 regex <- search_pattern 544 text <- JEdit_Lib.get_text(buffer, line_range) 545 m <- regex.findAllMatchIn(text) 546 range = Text.Range(m.start, m.end) + line_range.start 547 r <- JEdit_Lib.gfx_range(text_area, range) 548 } { 549 gfx.setColor(rendering.search_color) 550 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 551 } 552 553 // highlight range -- potentially from other snapshot 554 for { 555 info <- highlight_area.info 556 Text.Info(range, color) <- info.try_restrict(line_range) 557 r <- JEdit_Lib.gfx_range(text_area, range) 558 } { 559 gfx.setColor(color) 560 gfx.fillRect(r.x, y + i * line_height, r.length, line_height) 561 } 562 563 // hyperlink range -- potentially from other snapshot 564 for { 565 info <- hyperlink_area.info 566 Text.Info(range, _) <- info.try_restrict(line_range) 567 r <- JEdit_Lib.gfx_range(text_area, range) 568 } { 569 gfx.setColor(rendering.hyperlink_color) 570 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) 571 } 572 573 // entity def range 574 if (!area_active() && caret_visible) { 575 for { 576 Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) 577 r <- JEdit_Lib.gfx_range(text_area, range) 578 } { 579 gfx.setColor(color) 580 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) 581 } 582 } 583 584 // completion range 585 if (!area_active() && caret_visible) { 586 for { 587 completion <- Completion_Popup.Text_Area(text_area) 588 Text.Info(range, color) <- completion.rendering(rendering, line_range) 589 r <- JEdit_Lib.gfx_range(text_area, range) 590 } { 591 gfx.setColor(color) 592 gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) 593 } 594 } 595 } 596 } 597 } 598 } 599 } 600 601 602 /* caret -- outside of text range */ 603 604 private class Caret_Painter(before: Boolean) extends TextAreaExtension 605 { 606 override def paintValidLine(gfx: Graphics2D, 607 screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) 608 { 609 robust_rendering { _ => 610 if (before) gfx.clipRect(0, 0, 0, 0) 611 else gfx.setClip(painter_clip) 612 } 613 } 614 } 615 616 private val before_caret_painter1 = new Caret_Painter(true) 617 private val after_caret_painter1 = new Caret_Painter(false) 618 private val before_caret_painter2 = new Caret_Painter(true) 619 private val after_caret_painter2 = new Caret_Painter(false) 620 621 private val caret_painter = new TextAreaExtension 622 { 623 override def paintValidLine(gfx: Graphics2D, 624 screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) 625 { 626 robust_rendering { rendering => 627 if (caret_visible) { 628 val caret = text_area.getCaretPosition 629 if (caret_enabled && start <= caret && caret == end - 1) { 630 val painter = text_area.getPainter 631 val fm = painter.getFontMetrics 632 633 val offset = caret - text_area.getLineStartOffset(physical_line) 634 val x = text_area.offsetToXY(physical_line, offset).x 635 val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent 636 637 val astr = new AttributedString(" ") 638 astr.addAttribute(TextAttribute.FONT, painter.getFont) 639 astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret)) 640 astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) 641 642 val clip = gfx.getClip 643 try { 644 gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight) 645 gfx.drawString(astr.getIterator, x, y1) 646 } 647 finally { gfx.setClip(clip) } 648 } 649 } 650 } 651 } 652 } 653 654 655 /* activation */ 656 657 def activate() 658 { 659 val painter = text_area.getPainter 660 painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) 661 painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) 662 painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) 663 painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) 664 painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) 665 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) 666 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2) 667 painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) 668 painter.addExtension(500, foreground_painter) 669 painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state) 670 painter.removeExtension(orig_text_painter) 671 painter.addMouseListener(mouse_listener) 672 painter.addMouseMotionListener(mouse_motion_listener) 673 text_area.addFocusListener(focus_listener) 674 view.addWindowListener(window_listener) 675 } 676 677 def deactivate() 678 { 679 active_reset() 680 val painter = text_area.getPainter 681 view.removeWindowListener(window_listener) 682 text_area.removeFocusListener(focus_listener) 683 painter.removeMouseMotionListener(mouse_motion_listener) 684 painter.removeMouseListener(mouse_listener) 685 painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) 686 painter.removeExtension(reset_state) 687 painter.removeExtension(foreground_painter) 688 painter.removeExtension(caret_painter) 689 painter.removeExtension(after_caret_painter2) 690 painter.removeExtension(before_caret_painter2) 691 painter.removeExtension(after_caret_painter1) 692 painter.removeExtension(before_caret_painter1) 693 painter.removeExtension(text_painter) 694 painter.removeExtension(background_painter) 695 painter.removeExtension(set_state) 696 } 697} 698