Quelle rich_text_area.scala Sprache: Scala

/*  Title:      Tools/jEdit/src/rich_text_area.scala
    Author:     Makarius

Enhanced version of jEdit text area, with rich text rendering,
tooltips, hyperlinks etc.
*/

package isabelle.jedit

import isabelle._

import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo, Font}
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, KeyEvent}
import java.awt.font.TextAttribute
import javax.swing.SwingUtilities
import java.text.AttributedString

import scala.util.matching.Regex
import scala.collection.mutable

import org.gjt.sp.util.Log
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.syntax.{Chunk => JEditChunk, SyntaxStyle}
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea, Selection}

class Rich_Text_Area(
  view: View,
  text_area: TextArea,
  get_rendering: () => JEdit_Rendering,
  close_action: () => Unit,
  get_search_pattern: () => Option[Regex],
  caret_update: () => Unit,
  caret_visible: Boolean,
  enable_hovering: Boolean
) {
  private val buffer = text_area.getBuffer

  /* robust extension body */

  def check_robust_body: Boolean =
    GUI_Thread.require { buffer == text_area.getBuffer }

  def robust_body[A](default: A)(body: => A): A = {
    try {
      if (check_robust_body) body
      else {
        Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
        default
      }
    }
    catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
  }

  /* original painters */

  private def pick_extension(name: String): TextAreaExtension = {
    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
    match {
      case List(x) => x
      case _ => error("Expected exactly one " + name)
    }
  }

  private val orig_text_painter =
    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")

  /* caret focus modifier */

  @volatile private var caret_focus_modifier = false

  def caret_focus_range: Text.Range =
    if (caret_focus_modifier) Text.Range.full
    else JEdit_Lib.visible_range(text_area) getOrElse Text.Range.offside

  private val key_listener =
    JEdit_Lib.key_listener(
      key_pressed = { (evt: KeyEvent) =>
        val mod = PIDE.options.string("jedit_focus_modifier")
        val old = caret_focus_modifier
        caret_focus_modifier = (mod.nonEmpty && mod == JEdit_Lib.modifier_string(evt))
        if (caret_focus_modifier != old) caret_update()
      },
      key_released = { _ =>
        if (caret_focus_modifier) {
          caret_focus_modifier = false
          caret_update()
        }
      })

  /* common painter state */

  @volatile private var painter_rendering: JEdit_Rendering = null
  @volatile private var painter_clip: Shape = null
  @volatile private var painter_gfx_range: Text.Range => Option[JEdit_Lib.Gfx_Range] = null
  @volatile private var caret_focus = Rendering.Focus.empty

  private val set_state = new TextAreaExtension {
    override def paintScreenLineRange(
      gfx: Graphics2D,
      first_line: Int,
      last_line: Int,
      physical_lines: Array[Int],
      start: Array[Int],
      end: Array[Int],
      y: Int,
      line_height: Int
    ): Unit = {
      painter_rendering = get_rendering()
      painter_clip = gfx.getClip
      painter_gfx_range = JEdit_Lib.gfx_range(text_area)
      caret_focus =
        if (caret_enabled && !painter_rendering.snapshot.is_outdated) {
          painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), caret_focus_range)
        }
        else Rendering.Focus.empty
    }
  }

  private val reset_state = new TextAreaExtension {
    override def paintScreenLineRange(
      gfx: Graphics2D,
      first_line: Int,
      last_line: Int,
      physical_lines: Array[Int],
      start: Array[Int],
      end: Array[Int],
      y: Int,
      line_height: Int
    ): Unit = {
      painter_rendering = null
      painter_clip = null
      painter_gfx_range = null
      caret_focus = Rendering.Focus.empty
    }
  }

  def robust_rendering(body: JEdit_Rendering => Unit): Unit = {
    robust_body(()) { body(painter_rendering) }
  }

  /* active areas within the text */

  private class Active_Area[A](
    render: JEdit_Rendering => Text.Range => Option[Text.Info[A]],
    require_control: => Boolean = false,
    ignore_control: => Boolean = false,
    cursor: Int = -1
  ) {
    private var the_text_info: Option[(String, Text.Info[A])] = None

    def check_control(control: Boolean): Boolean =
      control == require_control || ignore_control

    def is_active: Boolean = the_text_info.isDefined
    def text_info: Option[(String, Text.Info[A])] = the_text_info
    def info: Option[Text.Info[A]] = the_text_info.map(_._2)

    def update(new_info: Option[Text.Info[A]]): Unit = {
      val old_text_info = the_text_info
      val new_text_info =
        for {
          info <- new_info
          s <- JEdit_Lib.get_text(text_area.getBuffer, info.range)
        } yield (s, info)

      if (new_text_info != old_text_info) {
        caret_update()
        if (cursor >= 0) {
          if (new_text_info.isDefined) {
            text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor))
          }
          else text_area.getPainter.resetCursor()
        }
        for {
          r0 <- JEdit_Lib.visible_range(text_area)
          opt <- List(old_text_info, new_text_info)
          (_, Text.Info(r1, _)) <- opt
          r2 <- r1.try_restrict(r0)  // FIXME more precise?!
        } JEdit_Lib.invalidate_range(text_area, r2)
        the_text_info = new_text_info
      }
    }

    def update_rendering(rendering: JEdit_Rendering, range: Text.Range): Unit =
      update(render(rendering)(range))

    def reset(): Unit = update(None)
  }

  // owned by GUI thread

  private val highlight_area =
    new Active_Area[Color](_.highlight, require_control = true,
      ignore_control = JEdit_Options.auto_hovering())

  private val hyperlink_area =
    new Active_Area[PIDE.editor.Hyperlink](
      _.hyperlink, require_control = true, cursor = Cursor.HAND_CURSOR)

  private val active_area =
    new Active_Area[XML.Elem](_.active, cursor = Cursor.DEFAULT_CURSOR)

  private val active_areas = List(highlight_area, hyperlink_area, active_area)
  private def active_exists(): Boolean = active_areas.exists(_.is_active)
  def active_reset(): Unit = active_areas.foreach(_.reset())

  private val focus_listener = new FocusAdapter {
    override def focusLost(e: FocusEvent): Unit = { robust_body(()) { active_reset() } }
  }

  private val window_listener = new WindowAdapter {
    override def windowIconified(e: WindowEvent): Unit = { robust_body(()) { active_reset() } }
    override def windowDeactivated(e: WindowEvent): Unit = { robust_body(()) { active_reset() } }
  }

  private val mouse_listener = new MouseAdapter {
    override def mousePressed(e: MouseEvent): Unit = {
      robust_body(()) {
        if (!e.isConsumed() && e.getClickCount == 1) {
          hyperlink_area.info match {
            case Some(Text.Info(range, link)) =>
              if (!link.external) {
                try {
                  text_area.moveCaretPosition(range.start)
                  PIDE.plugin.navigator.record(Isabelle_Navigator.Pos(buffer, range.start))
                }
                catch {
                  case _: ArrayIndexOutOfBoundsException =>
                  case _: IllegalArgumentException =>
                }
                text_area.requestFocus()
              }
              link.follow(view)
              e.consume()
            case None =>
          }
          active_area.text_info match {
            case Some((text, Text.Info(_, markup))) =>
              Active.action(view, text, markup)
              close_action()
              e.consume()
            case None =>
          }
        }
      }
    }
  }

  private def mouse_inside_painter(): Boolean =
    MouseInfo.getPointerInfo match {
      case null => false
      case info =>
        val point = info.getLocation
        val painter = text_area.getPainter
        SwingUtilities.convertPointFromScreen(point, painter)
        painter.contains(point)
    }

  private val mouse_motion_listener = new MouseMotionAdapter {
    override def mouseDragged(evt: MouseEvent): Unit = {
      robust_body(()) {
        active_reset()
        Completion_Popup.Text_Area.dismissed(text_area)
        Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
      }
    }

    override def mouseMoved(evt: MouseEvent): Unit = {
      robust_body(()) {
        val x = evt.getX
        val y = evt.getY
        val control = JEdit_Lib.command_modifier(evt)

        if ((control || enable_hovering) && !buffer.isLoading) {
          JEdit_Lib.buffer_lock(buffer) {
            JEdit_Lib.pixel_range(text_area, x, y) match {
              case None => active_reset()
              case Some(range) =>
                val rendering = get_rendering()
                for (area <- active_areas) {
                  if (area.check_control(control) && !rendering.snapshot.is_outdated) {
                    area.update_rendering(rendering, range)
                  }
                  else area.reset()
                }
                if (JEdit_Lib.alt_modifier(evt)) {
                  highlight_area.info.map(_.range) match {
                    case Some(range) =>
                      text_area.requestFocus()
                      text_area.selectNone()
                      text_area.addToSelection(new Selection.Range(range.start, range.stop))
                    case None =>
                  }
                }
            }
          }
        }
        else active_reset()

        if (evt.getSource == text_area.getPainter) {
          Pretty_Tooltip.invoke(() =>
            robust_body(()) {
              if (mouse_inside_painter()) {
                val rendering = get_rendering()
                val snapshot = rendering.snapshot
                if (!snapshot.is_outdated) {
                  JEdit_Lib.pixel_range(text_area, x, y) match {
                    case None =>
                    case Some(range) =>
                      rendering.tooltip(range, control) match {
                        case None =>
                        case Some(tip) =>
                          val painter = text_area.getPainter
                          val loc = new Point(x, y + painter.getLineHeight / 2)
                          val results = snapshot.command_results(tip.range)
                          Pretty_Tooltip(view, painter, loc, rendering, results, tip.info)
                      }
                  }
                }
              }
          })
        }
      }
    }
  }

  /* text background */

  private val background_painter = new TextAreaExtension {
    override def paintScreenLineRange(
      gfx: Graphics2D,
      first_line: Int,
      last_line: Int,
      physical_lines: Array[Int],
      start: Array[Int],
      end: Array[Int],
      y: Int,
      line_height: Int
    ): Unit = {
      robust_rendering { rendering =>
        val fm = text_area.getPainter.getFontMetrics

        for (i <- physical_lines.indices) {
          if (physical_lines(i) != -1) {
            val line_range = Text.Range(start(i), end(i) min buffer.getLength)

            // line background color
            for (c <- rendering.line_background(line_range)) {
              val separator = rendering.line_separator(line_range)
              val sep = if (separator) (2 min (line_height / 2)) max (line_height / 8) else 0
              gfx.setColor(rendering.color(c))
              gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
            }

            // background color
            for {
              Text.Info(range, c) <-
                rendering.background(Rendering.background_elements, line_range, caret_focus)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(rendering.color(c))
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
            }

            // active area -- potentially from other snapshot
            for {
              info <- active_area.info
              Text.Info(range, _) <- info.try_restrict(line_range)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(rendering.active_hover_color)
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
            }

            // squiggly underline
            for {
              Text.Info(range, c) <- rendering.squiggly_underline(line_range)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(rendering.color(c))
              val x0 = (r.x / 2) * 2
              val y0 = r.y + fm.getAscent + 1
              for (x1 <- Range(x0, x0 + r.length, 2)) {
                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
                gfx.drawLine(x1, y1, x1 + 1, y1)
              }
            }

            // spell checker
            for {
              spell_checker <- PIDE.plugin.spell_checker.get
              spell <- rendering.spell_checker(line_range)
              text <- JEdit_Lib.get_text(buffer, spell.range)
              info <- spell_checker.marked_words(spell.range.start, text)
              r <- painter_gfx_range(info.range)
            } {
              gfx.setColor(rendering.spell_checker_color)
              val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2))
              gfx.drawLine(r.x, y0, r.x + r.length, y0)
            }
          }
        }
      }
    }
  }

  /* text */

  private def caret_enabled: Boolean =
    caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)

  private def caret_color(rendering: JEdit_Rendering, offset: Text.Offset): Color = {
    if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
    else {
      val debug_positions =
        (for {
          c <- PIDE.session.debugger.focus().iterator
          pos <- c.debug_position.iterator
        } yield pos).toList
      if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
        rendering.caret_debugger_color
      else rendering.caret_invisible_color
    }
  }

  private class Font_Subst {
    private var cache = Map.empty[Int, Option[Font]]

    def get(codepoint: Int): Option[Font] =
      cache.getOrElse(codepoint,
        {
          val field = classOf[JEditChunk].getDeclaredField("lastSubstFont")
          field.setAccessible(true)
          field.set(null, null)
          val res = Option(JEditChunk.getSubstFont(codepoint))
          cache += (codepoint -> res)
          res
        })
  }

  sealed case class Chunk(
    id: Byte,
    style: SyntaxStyle,
    offset: Int,
    length: Int,
    width: Float,
    font_subst: Boolean,
    str: String
  )

  private def make_chunk_list(chunk_head: JEditChunk): List[Chunk] = {
    val buf = new mutable.ListBuffer[Chunk]
    var chunk = chunk_head
    while (chunk != null) {
      val str =
        if (chunk.chars == null) Symbol.spaces(chunk.length)
        else {
          if (chunk.str == null) { chunk.str = new String(chunk.chars) }
          chunk.str
        }
      buf += Chunk(chunk.id, chunk.style, chunk.offset, chunk.length, chunk.width,
        chunk.usedFontSubstitution, str)
      chunk = chunk.next.asInstanceOf[JEditChunk]
    }
    buf.toList
  }

  private def paint_chunk_list(
    rendering: JEdit_Rendering,
    font_subst: Font_Subst,
    gfx: Graphics2D,
    line_start: Text.Offset,
    caret_range: Text.Range,
    chunk_list: List[Chunk],
    x0: Int,
    y0: Int
  ): Float = {
    val clip_rect = gfx.getClipBounds

    val x = x0.toFloat
    val y = y0.toFloat
    chunk_list.foldLeft(0.0f) { case (w, chunk) =>
      val chunk_offset = line_start + chunk.offset
      if (x + w + chunk.width > clip_rect.x &&
          x + w < clip_rect.x + clip_rect.width && chunk.length > 0) {
        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
        val chunk_font = chunk.style.getFont
        val chunk_color = chunk.style.getForegroundColor
        val chunk_text = new AttributedString(chunk.str)

        def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit =
          chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset)

        // font
        chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
        chunk_text.addAttribute(TextAttribute.FONT, chunk_font)
        if (chunk.font_subst) {
          for {
            (c, i) <- Codepoint.iterator_offset(chunk.str) if !chunk_font.canDisplay(c)
            subst_font <- font_subst.get(c)
          } {
            val r = Text.Range(i, i + Character.charCount(c)) + chunk_offset
            val font = JEditChunk.deriveSubstFont(chunk_font, subst_font)
            chunk_attrib(TextAttribute.FONT, font, r)
          }
        }

        // color
        chunk_text.addAttribute(TextAttribute.FOREGROUND, chunk_color)
        for {
          Text.Info(r1, color) <- rendering.text_color(chunk_range, chunk_color).iterator
          r2 <- r1.try_restrict(chunk_range) if !r2.is_singularity
        } chunk_attrib(TextAttribute.FOREGROUND, color, r2)

        // caret
        for { r <- caret_range.try_restrict(chunk_range) if !r.is_singularity } {
          chunk_attrib(TextAttribute.FOREGROUND, caret_color(rendering, r.start), r)
          chunk_attrib(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, r)
        }

        gfx.drawString(chunk_text.getIterator, x + w, y)
      }
      w + chunk.width
    }
  }

  private val text_painter = new TextAreaExtension {
    override def paintScreenLineRange(
      gfx: Graphics2D,
      first_line: Int,
      last_line: Int,
      physical_lines: Array[Int],
      start: Array[Int],
      end: Array[Int],
      y: Int,
      line_height: Int
    ): Unit = {
      robust_rendering { rendering =>
        val painter = text_area.getPainter
        val fm = painter.getFontMetrics
        val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)

        val clip = gfx.getClip
        val x0 = text_area.getHorizontalOffset
        var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent

        val (bullet_x, bullet_y, bullet_w, bullet_h) = {
          val w = fm.charWidth(' ')
          val b = (w / 2) max 1
          val c = (lm.getAscent + lm.getStrikethroughOffset).round
          ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
        }

        val font_subst = new Font_Subst

        for (i <- physical_lines.indices) {
          val line = physical_lines(i)
          if (line != -1) {
            val line_range = Text.Range(start(i), end(i) min buffer.getLength)

            // text chunks
            val screen_line = first_line + i
            val chunk_list = make_chunk_list(text_area.getChunksOfScreenLine(screen_line))
            if (chunk_list.nonEmpty) {
              try {
                val line_start = buffer.getLineStartOffset(line)
                val caret_range =
                  if (caret_enabled) JEdit_Lib.caret_range(text_area)
                  else Text.Range.offside
                gfx.clipRect(x0, y + line_height * i, Int.MaxValue, line_height)
                val w =
                  paint_chunk_list(rendering, font_subst, gfx,
                    line_start, caret_range, chunk_list, x0, y0)
                gfx.clipRect(x0 + w.toInt, 0, Int.MaxValue, Int.MaxValue)
                orig_text_painter.paintValidLine(gfx,
                  screen_line, line, start(i), end(i), y + line_height * i)
              } finally { gfx.setClip(clip) }
            }

            // bullet bar
            for {
              Text.Info(range, color) <- rendering.bullet(line_range)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(color)
              gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
                r.length - bullet_w, line_height - bullet_h)
            }
          }
          y0 += line_height
        }
      }
    }
  }

  /* foreground */

  private val foreground_painter = new TextAreaExtension {
    override def paintScreenLineRange(
      gfx: Graphics2D,
      first_line: Int,
      last_line: Int,
      physical_lines: Array[Int],
      start: Array[Int],
      end: Array[Int],
      y: Int,
      line_height: Int
    ): Unit = {
      robust_rendering { rendering =>
        val search_pattern = get_search_pattern()
        for (i <- physical_lines.indices) {
          if (physical_lines(i) != -1) {
            val line_range = Text.Range(start(i), end(i) min buffer.getLength)

            // foreground color
            for {
              Text.Info(range, c) <- rendering.foreground(line_range)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(rendering.color(c))
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
            }

            // search pattern
            for {
              regex <- search_pattern
              range <- JEdit_Lib.search_text(buffer, line_range, regex)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(rendering.search_color)
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
            }

            // highlight range -- potentially from other snapshot
            for {
              info <- highlight_area.info
              Text.Info(range, color) <- info.try_restrict(line_range)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(color)
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
            }

            // hyperlink range -- potentially from other snapshot
            for {
              info <- hyperlink_area.info
              Text.Info(range, _) <- info.try_restrict(line_range)
              r <- painter_gfx_range(range)
            } {
              gfx.setColor(rendering.hyperlink_color)
              gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
            }

            // entity def range
            if (!active_exists() && caret_visible) {
              for {
                Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus)
                r <- painter_gfx_range(range)
              } {
                gfx.setColor(color)
                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
              }
            }

            // completion range
            if (!active_exists() && caret_visible) {
              for {
                completion <- Completion_Popup.Text_Area(text_area)
                Text.Info(range, color) <- completion.rendering(rendering, line_range)
                r <- painter_gfx_range(range)
              } {
                gfx.setColor(color)
                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
              }
            }
          }
        }
      }
    }
  }

  /* caret -- outside of text range */

  private class Caret_Painter(before: Boolean) extends TextAreaExtension {
    override def paintValidLine(
      gfx: Graphics2D,
      screen_line: Int,
      physical_line: Int,
      start: Int,
      end: Int,
      y: Int
    ): Unit = {
      robust_rendering { _ =>
        if (before) gfx.clipRect(0, 0, 0, 0)
        else gfx.setClip(painter_clip)
      }
    }
  }

  private val before_caret_painter1 = new Caret_Painter(true)
  private val after_caret_painter1 = new Caret_Painter(false)
  private val before_caret_painter2 = new Caret_Painter(true)
  private val after_caret_painter2 = new Caret_Painter(false)

  private val caret_painter = new TextAreaExtension {
    override def paintValidLine(
      gfx: Graphics2D,
      screen_line: Int,
      physical_line: Int,
      start: Int,
      end: Int,
      y: Int
    ): Unit = {
      robust_rendering { rendering =>
        if (caret_visible) {
          val caret = text_area.getCaretPosition
          if (caret_enabled && start <= caret && caret == end - 1) {
            val painter = text_area.getPainter
            val fm = painter.getFontMetrics

            val offset = caret - text_area.getLineStartOffset(physical_line)
            val x = text_area.offsetToXY(physical_line, offset).x
            val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent

            val astr = new AttributedString(" ")
            astr.addAttribute(TextAttribute.FONT, painter.getFont)
            astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret))
            astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)

            val clip = gfx.getClip
            try {
              gfx.clipRect(x, y, Int.MaxValue, painter.getLineHeight)
              gfx.drawString(astr.getIterator, x, y1)
            }
            finally { gfx.setClip(clip) }
          }
        }
      }
    }
  }

  /* activation */

  def activate(): Unit = {
    val painter = text_area.getPainter
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
    painter.addExtension(500, foreground_painter)
    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
    painter.removeExtension(orig_text_painter)
    painter.addMouseListener(mouse_listener)
    painter.addMouseMotionListener(mouse_motion_listener)
    text_area.addKeyListener(key_listener)
    text_area.addFocusListener(focus_listener)
    view.addWindowListener(window_listener)
  }

  def deactivate(): Unit = {
    active_reset()
    val painter = text_area.getPainter
    view.removeWindowListener(window_listener)
    text_area.removeFocusListener(focus_listener)
    text_area.removeKeyListener(key_listener)
    painter.removeMouseMotionListener(mouse_motion_listener)
    painter.removeMouseListener(mouse_listener)
    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
    painter.removeExtension(reset_state)
    painter.removeExtension(foreground_painter)
    painter.removeExtension(caret_painter)
    painter.removeExtension(after_caret_painter2)
    painter.removeExtension(before_caret_painter2)
    painter.removeExtension(after_caret_painter1)
    painter.removeExtension(before_caret_painter1)
    painter.removeExtension(text_painter)
    painter.removeExtension(background_painter)
    painter.removeExtension(set_state)
  }
}

quality87%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.