src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Sat Mar 23 13:12:39 2013 +0100 (2013-03-23)
changeset 51492 eaa1c4cc1106
parent 51469 18120e26f818
child 51507 ebd5366e7a42
permissions -rw-r--r--
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
     2     Author:     Makarius
     3 
     4 Misc library functions for jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
    13 
    14 import scala.annotation.tailrec
    15 
    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}
    19 
    20 
    21 object JEdit_Lib
    22 {
    23   /* bounds within multi-screen environment */
    24 
    25   def screen_bounds(screen_point: Point): Rectangle =
    26   {
    27     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
    28     (for {
    29       device <- ge.getScreenDevices.iterator
    30       config <- device.getConfigurations.iterator
    31       bounds = config.getBounds
    32     } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
    33   }
    34 
    35 
    36   /* GUI components */
    37 
    38   def get_parent(component: Component): Option[Container] =
    39     component.getParent match {
    40       case null => None
    41       case parent => Some(parent)
    42     }
    43 
    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 =
    48       next_elem match {
    49         case Some(parent) =>
    50           next_elem = get_parent(parent)
    51           parent
    52         case None => Iterator.empty.next()
    53       }
    54   }
    55 
    56   def parent_window(component: Component): Option[Window] =
    57     ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
    58 
    59 
    60   /* basic tooltips, with multi-line support */
    61 
    62   def wrap_tooltip(text: String): String =
    63     if (text == "") null
    64     else "<html><pre>" + HTML.encode(text) + "</pre></html>"
    65 
    66 
    67   /* buffers */
    68 
    69   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    70     Swing_Thread.now { buffer_lock(buffer) { body } }
    71 
    72   def buffer_text(buffer: JEditBuffer): String =
    73     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    74 
    75   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    76 
    77 
    78   /* main jEdit components */
    79 
    80   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    81 
    82   def jedit_buffer(name: String): Option[Buffer] =
    83     jedit_buffers().find(buffer => buffer_name(buffer) == name)
    84 
    85   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    86 
    87   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    88     view.getEditPanes().iterator.map(_.getTextArea)
    89 
    90   def jedit_text_areas(): Iterator[JEditTextArea] =
    91     jedit_views().flatMap(jedit_text_areas(_))
    92 
    93   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
    94     jedit_text_areas().filter(_.getBuffer == buffer)
    95 
    96   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    97   {
    98     try { buffer.readLock(); body }
    99     finally { buffer.readUnlock() }
   100   }
   101 
   102   def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
   103   {
   104     try { buffer.beginCompoundEdit(); body }
   105     finally { buffer.endCompoundEdit() }
   106   }
   107 
   108 
   109   /* get text */
   110 
   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 }
   114 
   115 
   116   /* buffer range */
   117 
   118   def buffer_range(buffer: JEditBuffer): Text.Range =
   119     Text.Range(0, (buffer.getLength - 1) max 0)
   120 
   121 
   122   /* point range */
   123 
   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)
   127       try {
   128         val c = text(offset)
   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)
   134       }
   135       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
   136     }
   137 
   138 
   139   /* visible text range */
   140 
   141   def visible_range(text_area: TextArea): Option[Text.Range] =
   142   {
   143     val buffer = text_area.getBuffer
   144     val n = text_area.getVisibleLines
   145     if (n > 0) {
   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))
   150     }
   151     else None
   152   }
   153 
   154   def invalidate_range(text_area: TextArea, range: Text.Range)
   155   {
   156     val buffer = text_area.getBuffer
   157     text_area.invalidateLineRange(
   158       buffer.getLineOfOffset(range.start),
   159       buffer.getLineOfOffset(range.stop))
   160   }
   161 
   162 
   163   /* graphics range */
   164 
   165   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
   166 
   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] =
   170   {
   171     val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
   172     val char_width = (metric.unit * metric.average).round.toInt
   173 
   174     val buffer = text_area.getBuffer
   175 
   176     val end = buffer.getLength
   177     val stop = range.stop
   178 
   179     val (p, q, r) =
   180       try {
   181         val p = text_area.offsetToXY(range.start)
   182         val (q, r) =
   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)
   187         (p, q, r)
   188       }
   189       catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
   190 
   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))
   193     else None
   194   }
   195 
   196 
   197   /* pixel range */
   198 
   199   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   200   {
   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)
   204       case _ => None
   205     }
   206   }
   207 
   208 
   209   /* pretty text metric */
   210 
   211   def string_width(painter: TextAreaPainter, s: String): Double =
   212     painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
   213 
   214   def pretty_metric(painter: TextAreaPainter): Pretty.Metric =
   215     new 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
   219     }
   220 }
   221