more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);
/* Title: Tools/jEdit/src/jedit_lib.scala Author: MakariusMisc library functions for jEdit.*/package isabelle.jeditimport isabelle._import java.io.{File => JFile}import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}import java.awt.event.{InputEvent, KeyEvent, KeyListener}import javax.swing.{Icon, ImageIcon, JScrollBar, JWindow, SwingUtilities}import scala.util.parsing.input.CharSequenceReaderimport scala.jdk.CollectionConverters._import scala.annotation.tailrecimport org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}import org.gjt.sp.jedit.io.{FileVFS, VFSManager}import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection}object JEdit_Lib { /* jEdit directories */ def directories: List[JFile] = (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_)) /* window geometry measurement */ private lazy val dummy_window = new JWindow final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) { def deco_width: Int = width - inner_width def deco_height: Int = height - inner_height } def window_geometry(outer: Container, inner: Component): Window_Geometry = { GUI_Thread.require {} val old_content = dummy_window.getContentPane dummy_window.setContentPane(outer) dummy_window.pack() dummy_window.revalidate() val geometry = Window_Geometry( dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight) dummy_window.setContentPane(old_content) geometry } /* plain files */ def is_file(name: String): Boolean = name != null && name.nonEmpty && VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] def check_file(name: String): Option[JFile] = if (is_file(name)) Some(new JFile(name)) else None /* buffers */ def buffer_text(buffer: JEditBuffer): String = buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } def buffer_reader(buffer: JEditBuffer): CharSequenceReader = Scan.char_reader(buffer.getSegment(0, buffer.getLength)) def buffer_mode(buffer: JEditBuffer): String = { val mode = buffer.getMode if (mode == null) "" else { val name = mode.getName if (name == null) "" else name } } def buffer_line_manager(buffer: JEditBuffer): LineManager = Untyped.get[LineManager](buffer, "lineMgr") def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer)) /* main jEdit components */ def jedit_buffers(): Iterator[Buffer] = jEdit.getBufferManager().getBuffers().asScala.iterator def jedit_buffer(name: String): Option[Buffer] = jedit_buffers().find(buffer => buffer_name(buffer) == name) def jedit_buffer(name: Document.Node.Name): Option[Buffer] = jedit_buffer(name.node) def jedit_views(): Iterator[View] = jEdit.getViewManager().getViews().asScala.iterator def jedit_view(view: View = null): View = if (view == null) jEdit.getActiveView() else view def jedit_edit_panes(view: View): Iterator[EditPane] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null) def jedit_text_areas(view: View): Iterator[JEditTextArea] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null) def jedit_text_areas(): Iterator[JEditTextArea] = jedit_views().flatMap(jedit_text_areas) def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = jedit_text_areas().filter(_.getBuffer == buffer) def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.readLock(); body } finally { buffer.readUnlock() } } def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.beginCompoundEdit(); body } finally { buffer.endCompoundEdit() } } /* buffer text */ def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = try { Some(buffer.getText(range.start, range.length)) } catch { case _: ArrayIndexOutOfBoundsException => None } def set_text(buffer: JEditBuffer, text: List[String]): Int = { val old = buffer.isUndoInProgress def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b) val length = buffer.getLength var offset = 0 @tailrec def drop_common_prefix(list: List[String]): List[String] = list match { case s :: rest if offset + s.length <= length && CharSequence.compare(buffer.getSegment(offset, s.length), s) == 0 => offset += s.length drop_common_prefix(rest) case _ => list } def insert(list: List[String]): Unit = for (s <- list) { buffer.insert(offset, s) offset += s.length } try { set(true) buffer.beginCompoundEdit() val rest = drop_common_prefix(text) val update_start = offset if (offset < length) buffer.remove(offset, length - offset) insert(rest) update_start } finally { buffer.endCompoundEdit() set(old) } } /* point range */ def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range = if (offset < 0) Text.Range.offside else buffer_lock(buffer) { def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) try { val c = text(offset) if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) Text.Range(offset, offset + 2) else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1))) Text.Range(offset - 1, offset + 1) else Text.Range(offset, offset + 1) } catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } } /* text ranges */ def buffer_range(buffer: JEditBuffer): Text.Range = Text.Range(0, buffer.getLength) def line_range(buffer: JEditBuffer, line: Int): Text.Range = Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength) def caret_range(text_area: TextArea): Text.Range = point_range(text_area.getBuffer, text_area.getCaretPosition) def selection_ranges(text_area: TextArea): List[Text.Range] = { val buffer = text_area.getBuffer text_area.getSelection.toList.flatMap( { case rect: Selection.Rect => List.from( for { l <- (rect.getStartLine to rect.getEndLine).iterator r = Text.Range(rect.getStart(buffer, l), rect.getEnd(buffer, l)) if !r.is_singularity } yield r) case sel: Selection => List(Text.Range(sel.getStart, sel.getEnd)) }) } def visible_range(text_area: TextArea): Option[Text.Range] = { val buffer = text_area.getBuffer val n = text_area.getVisibleLines if (n > 0) { val start = text_area.getScreenLineStartOffset(0) val raw_end = text_area.getScreenLineEndOffset(n - 1) val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength Some(Text.Range(start, end)) } else None } def invalidate_range(text_area: TextArea, range: Text.Range): Unit = { val buffer = text_area.getBuffer buffer_range(buffer).try_restrict(range) match { case Some(range1) if !range1.is_singularity => try { text_area.invalidateLineRange( buffer.getLineOfOffset(range1.start), buffer.getLineOfOffset(range1.stop)) } catch { case _: ArrayIndexOutOfBoundsException => } case _ => } } def invalidate_screen(text_area: TextArea, start: Int = -1, end: Int = -1): Unit = { val visible_lines = text_area.getVisibleLines 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) } } /* scrolling */ def vertical_scrollbar(text_area: TextArea): JScrollBar = Untyped.get[JScrollBar](text_area, "vertical") def horizontal_scrollbar(text_area: TextArea): JScrollBar = Untyped.get[JScrollBar](text_area, "horizontal") def scrollbar_at_end(scrollbar: JScrollBar): Boolean = scrollbar.getValue > 0 && scrollbar.getValue + scrollbar.getVisibleAmount == scrollbar.getMaximum def scrollbar_bottom(text_area: TextArea): Boolean = scrollbar_at_end(vertical_scrollbar(text_area)) def scrollbar_start(text_area: TextArea): Int = text_area.getBuffer.getLineStartOffset(vertical_scrollbar(text_area).getValue) def bottom_line_offset(buffer: JEditBuffer): Int = buffer.getLineStartOffset(buffer.getLineOfOffset(buffer.getLength)) def scroll_to_caret(text_area: TextArea): Unit = { val caret_line = text_area.getCaretLine() val display_manager = text_area.getDisplayManager if (!display_manager.isLineVisible(caret_line)) { display_manager.expandFold(caret_line, true) } text_area.scrollToCaret(true) } /* graphics range */ def font_metric(painter: TextAreaPainter): Font_Metric = new Font_Metric( font = painter.getFont, context = painter.getFontRenderContext) case class Gfx_Range(x: Int, y: Int, length: Int) // NB: jEdit always normalizes \r\n and \r to \n // NB: last line lacks \n def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = { val metric = font_metric(text_area.getPainter) val char_width = metric.average_width.round.toInt val buffer = text_area.getBuffer val end = buffer.getLength val stop = range.stop val (p, q, r) = try { val p = text_area.offsetToXY(range.start) val (q, r) = if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) { (text_area.offsetToXY(stop - 1), char_width) } else if (stop >= end) { (text_area.offsetToXY(end), char_width * (stop - end)) } else (text_area.offsetToXY(stop), 0) (p, q, r) } catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } if (p != null && q != null && p.x < q.x + r && p.y == q.y) { Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) } else None } /* pixel range */ def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = { // coordinates wrt. inner painter component val painter = text_area.getPainter if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) { val offset = text_area.xyToOffset(x, y, false) if (offset >= 0) { val range = point_range(text_area.getBuffer, offset) gfx_range(text_area, range) match { case Some(g) if g.x <= x && x < g.x + g.length => Some(range) case _ => None } } else None } else None } /* icons */ def load_icon(name: String): Icon = { val name1 = if (name.startsWith("idea-icons/")) { val file = File.uri(Path.explode("$ISABELLE_IDEA_ICONS")).toASCIIString "jar:" + file + "!/" + name } else name val icon = GUIUtilities.loadIcon(name1) if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name) else icon } def load_image_icon(name: String): ImageIcon = load_icon(name) match { case icon: ImageIcon => icon case _ => error("Bad image icon: " + name) } /* key event handling */ def request_focus_view(alt_view: View = null): Unit = { val view = if (alt_view != null) alt_view else jEdit.getActiveView() if (view != null) { val text_area = view.getTextArea if (text_area != null) text_area.requestFocus() } } def propagate_key(view: View, evt: KeyEvent): Unit = { if (view != null && !evt.isConsumed) view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false) } def key_listener( key_typed: KeyEvent => Unit = _ => (), key_pressed: KeyEvent => Unit = _ => (), key_released: KeyEvent => Unit = _ => () ): KeyListener = { def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit): Unit = { val evt = KeyEventWorkaround.processKeyEvent(evt0) if (evt != null) handle(evt) } new KeyListener { def keyTyped(evt: KeyEvent): Unit = process_key_event(evt, key_typed) def keyPressed(evt: KeyEvent): Unit = process_key_event(evt, key_pressed) def keyReleased(evt: KeyEvent): Unit = process_key_event(evt, key_released) } } def special_key(evt: KeyEvent): Boolean = { // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java val mod = evt.getModifiersEx (mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 || (mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED || (mod & InputEvent.META_DOWN_MASK) != 0 } def command_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 def shift_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0 def alt_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & InputEvent.ALT_DOWN_MASK) != 0 def modifier_string(evt: InputEvent): String = KeyEventTranslator.getModifierString(evt) match { case null => "" case s => s }}