def buffer_mode(buffer: JEditBuffer): String = { val mode = buffer.getMode if (mode == null) "" else { val name = mode.getName if (name == null) ""else name
}
}
def search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): List[Text.Range] =
List.from( for {
s <- get_text(buffer, range).iterator
m <- regex.findAllMatchIn(s)
} yield Text.Range(range.start + m.start, range.start + m.end))
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)
}
}
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)
}
}
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)
}
/* font */
def init_font_context(view: View, painter: TextAreaPainter): Unit = {
painter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
painter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics")) val old = painter.getFontRenderContext
Untyped.set[FontRenderContext](painter, "fontRenderContext", new FontRenderContext(view.getGraphicsConfiguration.getDefaultTransform,
old.getAntiAliasingHint, old.getFractionalMetricsHint))
}
def font_metric(painter: TextAreaPainter): Font_Metric = new Font_Metric(
font = painter.getFont,
context = painter.getFontRenderContext)
/* graphics range */
caseclass 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): 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
{ (range: Text.Range) => val stop = range.stop 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)
} elseif (stop >= end) {
(text_area.offsetToXY(end), char_width * (stop - end))
} else (text_area.offsetToXY(stop), 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
} catch { case _: ArrayIndexOutOfBoundsException => 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 val buffer = text_area.getBuffer 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(buffer, offset)
gfx_range(text_area)(range) match { case Some(g) if g.x <= x && x < g.x + g.length =>
range.try_restrict(buffer_range(buffer)) case _ => None
}
} else None
} else None
}
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.
