# HG changeset patch # User wenzelm # Date 1720786736 -7200 # Node ID 38c63d4027c489a484608900dfd1af03b41679c2 # Parent 819402eeac3406a250db6f4066fe17d57b58e21a# Parent 69e21910febcea524929be57240dd6e3244490e5 merged diff -r 819402eeac34 -r 38c63d4027c4 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Pure/GUI/gui.scala Fri Jul 12 14:18:56 2024 +0200 @@ -13,7 +13,7 @@ import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute} import java.awt.geom.AffineTransform import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, - JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities} + RootPaneContainer, JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities} import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator, Orientation} @@ -365,13 +365,11 @@ } def parent_window(component: Component): Option[Window] = - ancestors(component).collectFirst({ case x: Window => x }) + ancestors(component).collectFirst({ case c: Window => c }) def layered_pane(component: Component): Option[JLayeredPane] = parent_window(component) match { - case Some(w: JWindow) => Some(w.getLayeredPane) - case Some(w: JFrame) => Some(w.getLayeredPane) - case Some(w: JDialog) => Some(w.getLayeredPane) + case Some(c: RootPaneContainer) => Some(c.getLayeredPane) case _ => None } diff -r 819402eeac34 -r 38c63d4027c4 src/Pure/GUI/popup.scala --- a/src/Pure/GUI/popup.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Pure/GUI/popup.scala Fri Jul 12 14:18:56 2024 +0200 @@ -22,7 +22,7 @@ component.setSize(size) component.setPreferredSize(size) component.setOpaque(true) - layered.add(component, JLayeredPane.DEFAULT_LAYER) + layered.add(component, JLayeredPane.POPUP_LAYER) layered.moveToFront(component) layered.repaint(component.getBounds()) } diff -r 819402eeac34 -r 38c63d4027c4 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Pure/General/symbol.scala Fri Jul 12 14:18:56 2024 +0200 @@ -51,6 +51,7 @@ def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9' + def is_ascii_digit(b: Byte): Boolean = is_ascii_digit(b.toChar) def is_ascii_hex(c: Char): Boolean = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f' diff -r 819402eeac34 -r 38c63d4027c4 src/Pure/General/value.scala --- a/src/Pure/General/value.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Pure/General/value.scala Fri Jul 12 14:18:56 2024 +0200 @@ -22,7 +22,7 @@ object Nat { def unapply(bs: Bytes): Option[scala.Int] = - if (bs.byte_iterator.forall(b => '0' <= b && b <= '9')) unapply(bs.text) + if (bs.byte_iterator.forall(Symbol.is_ascii_digit)) unapply(bs.text) else None def unapply(s: java.lang.String): Option[scala.Int] = s match { diff -r 819402eeac34 -r 38c63d4027c4 src/Pure/PIDE/byte_message.scala --- a/src/Pure/PIDE/byte_message.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Pure/PIDE/byte_message.scala Fri Jul 12 14:18:56 2024 +0200 @@ -44,7 +44,7 @@ builder += c.toByte } } - if (c == -1 && line.size == 0) None else Some(line.trim_line) + if (c == -1 && line.is_empty) None else Some(line.trim_line) } @@ -82,7 +82,7 @@ Value.Long.unapply(str).isDefined private def is_length(msg: Bytes): Boolean = - !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) && + !msg.is_empty && msg.byte_iterator.forall(Symbol.is_ascii_digit) && Value.Long.unapply(msg.text).isDefined def write_line_message(stream: OutputStream, msg: Bytes): Unit = { diff -r 819402eeac34 -r 38c63d4027c4 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Fri Jul 12 14:18:56 2024 +0200 @@ -196,7 +196,7 @@ private val delay_caret_update = Delay.last(PIDE.session.input_delay, gui = true) { session.caret_focus.post(Session.Caret_Focus) - JEdit_Lib.invalidate(text_area) + JEdit_Lib.invalidate_screen(text_area) } private val caret_listener = new CaretListener { @@ -229,7 +229,7 @@ changed.commands.exists(snapshot.node.commands.contains))) text_overview.foreach(_.invoke()) - JEdit_Lib.invalidate(text_area) + JEdit_Lib.invalidate_screen(text_area) } } } diff -r 819402eeac34 -r 38c63d4027c4 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Jul 12 14:18:56 2024 +0200 @@ -205,9 +205,13 @@ } } - def invalidate(text_area: TextArea): Unit = { + def invalidate_screen(text_area: TextArea, start: Int = -1, end: Int = -1): Unit = { val visible_lines = text_area.getVisibleLines - if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) + if (visible_lines > 0) { + val start_line = if (start >= 0) start else 0 + val end_line = if (end >= 0) end else visible_lines + text_area.invalidateScreenLineRange(start_line, end_line) + } } diff -r 819402eeac34 -r 38c63d4027c4 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Wed Jul 10 17:42:48 2024 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Jul 12 14:18:56 2024 +0200 @@ -18,10 +18,11 @@ 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 +import org.gjt.sp.jedit.syntax.{Chunk => JEditChunk, SyntaxStyle} import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea} @@ -145,8 +146,9 @@ /* active areas within the text */ private class Active_Area[A]( - rendering: JEdit_Rendering => Text.Range => Option[Text.Info[A]], - cursor: Option[Int] + render: JEdit_Rendering => Text.Range => Option[Text.Info[A]], + val require_control: Boolean = false, + cursor: Int = -1 ) { private var the_text_info: Option[(String, Text.Info[A])] = None @@ -161,11 +163,11 @@ if (new_text_info != old_text_info) { caret_update() - if (cursor.isDefined) { - if (new_text_info.isDefined) - text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) - else - text_area.getPainter.resetCursor() + 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) @@ -177,8 +179,8 @@ } } - def update_rendering(r: JEdit_Rendering, range: Text.Range): Unit = - update(rendering(r)(range)) + def update_rendering(rendering: JEdit_Rendering, range: Text.Range): Unit = + update(render(rendering)(range)) def reset(): Unit = update(None) } @@ -186,23 +188,18 @@ // owned by GUI thread private val highlight_area = - new Active_Area[Color]( - (rendering: JEdit_Rendering) => rendering.highlight, None) + new Active_Area[Color](_.highlight, require_control = true) private val hyperlink_area = new Active_Area[PIDE.editor.Hyperlink]( - (rendering: JEdit_Rendering) => rendering.hyperlink, Some(Cursor.HAND_CURSOR)) + _.hyperlink, require_control = true, cursor = Cursor.HAND_CURSOR) private val active_area = - new Active_Area[XML.Elem]( - (rendering: JEdit_Rendering) => rendering.active, Some(Cursor.DEFAULT_CURSOR)) + new Active_Area[XML.Elem](_.active, cursor = Cursor.DEFAULT_CURSOR) - private val active_areas = - List((highlight_area, true), (hyperlink_area, true), (active_area, false)) - def active_reset(): Unit = active_areas.foreach(_._1.reset()) - - private def area_active(): Boolean = - active_areas.exists({ case (area, _) => area.is_active }) + 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() } } @@ -270,9 +267,10 @@ case None => active_reset() case Some(range) => val rendering = get_rendering() - for ((area, require_control) <- active_areas) { - if (control == require_control && !rendering.snapshot.is_outdated) + for (area <- active_areas) { + if (control == area.require_control && !rendering.snapshot.is_outdated) { area.update_rendering(rendering, range) + } else area.reset() } } @@ -413,47 +411,64 @@ def get(codepoint: Int): Option[Font] = cache.getOrElse(codepoint, { - val field = classOf[Chunk].getDeclaredField("lastSubstFont") + val field = classOf[JEditChunk].getDeclaredField("lastSubstFont") field.setAccessible(true) field.set(null, null) - val res = Option(Chunk.getSubstFont(codepoint)) + 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, - head: Chunk, - x: Float, - y: Float + caret_range: Text.Range, + chunk_list: List[Chunk], + x0: Int, + y0: Int ): Float = { val clip_rect = gfx.getClipBounds - val caret_range = - if (caret_enabled) JEdit_Lib.caret_range(text_area) - else Text.Range.offside - - var w = 0.0f - var chunk = head - while (chunk != null) { + 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_str = - if (chunk.chars == null) Symbol.spaces(chunk.length) - else { - if (chunk.str == null) { chunk.str = new String(chunk.chars) } - chunk.str - } val chunk_font = chunk.style.getFont val chunk_color = chunk.style.getForegroundColor - - val chunk_text = new AttributedString(chunk_str) + 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) @@ -461,13 +476,13 @@ // font chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR) chunk_text.addAttribute(TextAttribute.FONT, chunk_font) - if (chunk.usedFontSubstitution) { + if (chunk.font_subst) { for { - (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c) + (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 = Chunk.deriveSubstFont(chunk_font, subst_font) + val font = JEditChunk.deriveSubstFont(chunk_font, subst_font) chunk_attrib(TextAttribute.FONT, font, r) } } @@ -487,10 +502,8 @@ gfx.drawString(chunk_text.getIterator, x + w, y) } - w += chunk.width - chunk = chunk.next.asInstanceOf[Chunk] + w + chunk.width } - w } private val text_painter = new TextAreaExtension { @@ -529,14 +542,17 @@ // text chunks val screen_line = first_line + i - val chunks = text_area.getChunksOfScreenLine(screen_line) - if (chunks != null) { + 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, chunks, x0.toFloat, y0.toFloat) + 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) @@ -621,7 +637,7 @@ } // entity def range - if (!area_active() && caret_visible) { + if (!active_exists() && caret_visible) { for { Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) r <- JEdit_Lib.gfx_range(text_area, range) @@ -632,7 +648,7 @@ } // completion range - if (!area_active() && caret_visible) { + if (!active_exists() && caret_visible) { for { completion <- Completion_Popup.Text_Area(text_area) Text.Info(range, color) <- completion.rendering(rendering, line_range)