/* Title: Tools/jEdit/src/jedit_lib.scala
Author: Makarius
Misc library functions for jEdit.
*/
package isabelle.jedit
import isabelle._
import java.awt.{Component, Container, Frame, Window}
import scala.annotation.tailrec
import org.gjt.sp.jedit.{jEdit, Buffer, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
object JEdit_Lib
{
/* GUI components */
def get_parent(component: Component): Option[Container] =
component.getParent match {
case null => None
case parent => Some(parent)
}
def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
private var next_elem = get_parent(component)
def hasNext(): Boolean = next_elem.isDefined
def next(): Container =
next_elem match {
case Some(parent) =>
next_elem = get_parent(parent)
parent
case None => Iterator.empty.next()
}
}
def parent_window(component: Component): Option[Window] =
ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
def parent_frame(component: Component): Option[Frame] =
ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
/* basic tooltips, with multi-line support */
def wrap_tooltip(text: String): String =
if (text == "") null
else "<html><pre>" + HTML.encode(text) + "</pre></html>"
/* buffers */
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
Swing_Thread.now { buffer_lock(buffer) { body } }
def buffer_text(buffer: JEditBuffer): String =
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
{
val name = buffer_name(buffer)
Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
}
/* main jEdit components */
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
def jedit_buffer(name: String): Option[Buffer] =
jedit_buffers().find(buffer => buffer_name(buffer) == name)
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
view.getEditPanes().iterator.map(_.getTextArea)
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() }
}
/* point range */
def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
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) }
}
/* visible text range */
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)
{
val buffer = text_area.getBuffer
text_area.invalidateLineRange(
buffer.getLineOfOffset(range.start),
buffer.getLineOfOffset(range.stop))
}
/* char width */
def char_width(text_area: TextArea): Int =
{
val painter = text_area.getPainter
val font = painter.getFont
val font_context = painter.getFontRenderContext
font.getStringBounds(" ", font_context).getWidth.round.toInt
}
/* graphics range */
case class Gfx_Range(val x: Int, val y: Int, val 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 buffer = text_area.getBuffer
val p = text_area.offsetToXY(range.start)
val end = buffer.getLength
val stop = range.stop
val (q, r) =
if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
(text_area.offsetToXY(stop - 1), char_width(text_area))
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
}
/* pixel range */
def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
{
val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
gfx_range(text_area, range) match {
case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
case _ => None
}
}
}