more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
1 /* Title: Tools/jEdit/src/jedit_lib.scala
4 Misc library functions for jEdit.
12 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
14 import scala.annotation.tailrec
16 import org.gjt.sp.jedit.{jEdit, Buffer, View}
17 import org.gjt.sp.jedit.buffer.JEditBuffer
18 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
23 /* bounds within multi-screen environment */
25 def screen_bounds(screen_point: Point): Rectangle =
27 val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
29 device <- ge.getScreenDevices.iterator
30 config <- device.getConfigurations.iterator
31 bounds = config.getBounds
32 } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
38 def get_parent(component: Component): Option[Container] =
39 component.getParent match {
41 case parent => Some(parent)
44 def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
45 private var next_elem = get_parent(component)
46 def hasNext(): Boolean = next_elem.isDefined
47 def next(): Container =
50 next_elem = get_parent(parent)
52 case None => Iterator.empty.next()
56 def parent_window(component: Component): Option[Window] =
57 ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
60 /* basic tooltips, with multi-line support */
62 def wrap_tooltip(text: String): String =
64 else "<html><pre>" + HTML.encode(text) + "</pre></html>"
69 def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
70 Swing_Thread.now { buffer_lock(buffer) { body } }
72 def buffer_text(buffer: JEditBuffer): String =
73 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
75 def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
78 /* main jEdit components */
80 def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
82 def jedit_buffer(name: String): Option[Buffer] =
83 jedit_buffers().find(buffer => buffer_name(buffer) == name)
85 def jedit_views(): Iterator[View] = jEdit.getViews().iterator
87 def jedit_text_areas(view: View): Iterator[JEditTextArea] =
88 view.getEditPanes().iterator.map(_.getTextArea)
90 def jedit_text_areas(): Iterator[JEditTextArea] =
91 jedit_views().flatMap(jedit_text_areas(_))
93 def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
94 jedit_text_areas().filter(_.getBuffer == buffer)
96 def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
98 try { buffer.readLock(); body }
99 finally { buffer.readUnlock() }
102 def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
104 try { buffer.beginCompoundEdit(); body }
105 finally { buffer.endCompoundEdit() }
111 def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
112 try { Some(buffer.getText(range.start, range.length)) }
113 catch { case _: ArrayIndexOutOfBoundsException => None }
118 def buffer_range(buffer: JEditBuffer): Text.Range =
119 Text.Range(0, (buffer.getLength - 1) max 0)
124 def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
125 buffer_lock(buffer) {
126 def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
129 if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
130 Text.Range(offset, offset + 2)
131 else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
132 Text.Range(offset - 1, offset + 1)
133 else Text.Range(offset, offset + 1)
135 catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
139 /* visible text range */
141 def visible_range(text_area: TextArea): Option[Text.Range] =
143 val buffer = text_area.getBuffer
144 val n = text_area.getVisibleLines
146 val start = text_area.getScreenLineStartOffset(0)
147 val raw_end = text_area.getScreenLineEndOffset(n - 1)
148 val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
149 Some(Text.Range(start, end))
154 def invalidate_range(text_area: TextArea, range: Text.Range)
156 val buffer = text_area.getBuffer
157 text_area.invalidateLineRange(
158 buffer.getLineOfOffset(range.start),
159 buffer.getLineOfOffset(range.stop))
165 case class Gfx_Range(val x: Int, val y: Int, val length: Int)
167 // NB: jEdit always normalizes \r\n and \r to \n
168 // NB: last line lacks \n
169 def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
171 val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
172 val char_width = (metric.unit * metric.average).round.toInt
174 val buffer = text_area.getBuffer
176 val end = buffer.getLength
177 val stop = range.stop
181 val p = text_area.offsetToXY(range.start)
183 if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
184 else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
185 (text_area.offsetToXY(stop - 1), char_width)
186 else (text_area.offsetToXY(stop), 0)
189 catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
191 if (p != null && q != null && p.x < q.x + r && p.y == q.y)
192 Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
199 def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
201 val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
202 gfx_range(text_area, range) match {
203 case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
209 /* pretty text metric */
211 def string_width(painter: TextAreaPainter, s: String): Double =
212 painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
214 def pretty_metric(painter: TextAreaPainter): Pretty.Metric =
216 val unit = string_width(painter, Pretty.space)
217 val average = string_width(painter, "mix") / (3 * unit)
218 def apply(s: String): Double = if (s == "\n") 1.0 else string_width(painter, s) / unit