src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Mon Nov 26 16:16:47 2012 +0100 (2012-11-26 ago)
changeset 50215 97959912840a
parent 50195 863b1dfc396c
child 50363 2f8dc9e65401
permissions -rw-r--r--
more general sendback properties;
support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
     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, Frame, Window}
    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}
    19 
    20 
    21 object JEdit_Lib
    22 {
    23   /* GUI components */
    24 
    25   def get_parent(component: Component): Option[Container] =
    26     component.getParent match {
    27       case null => None
    28       case parent => Some(parent)
    29     }
    30 
    31   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
    32     private var next_elem = get_parent(component)
    33     def hasNext(): Boolean = next_elem.isDefined
    34     def next(): Container =
    35       next_elem match {
    36         case Some(parent) =>
    37           next_elem = get_parent(parent)
    38           parent
    39         case None => Iterator.empty.next()
    40       }
    41   }
    42 
    43   def parent_window(component: Component): Option[Window] =
    44     ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
    45 
    46   def parent_frame(component: Component): Option[Frame] =
    47     ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
    48 
    49 
    50   /* basic tooltips, with multi-line support */
    51 
    52   def wrap_tooltip(text: String): String =
    53     if (text == "") null
    54     else "<html><pre>" + HTML.encode(text) + "</pre></html>"
    55 
    56 
    57   /* buffers */
    58 
    59   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    60     Swing_Thread.now { buffer_lock(buffer) { body } }
    61 
    62   def buffer_text(buffer: JEditBuffer): String =
    63     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    64 
    65   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    66 
    67   def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
    68     Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
    69 
    70   def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    71   {
    72     val name = buffer_name(buffer)
    73     Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    74   }
    75 
    76 
    77   /* main jEdit components */
    78 
    79   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    80 
    81   def jedit_buffer(name: String): Option[Buffer] =
    82     jedit_buffers().find(buffer => buffer_name(buffer) == name)
    83 
    84   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    85 
    86   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    87     view.getEditPanes().iterator.map(_.getTextArea)
    88 
    89   def jedit_text_areas(): Iterator[JEditTextArea] =
    90     jedit_views().flatMap(jedit_text_areas(_))
    91 
    92   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
    93     jedit_text_areas().filter(_.getBuffer == buffer)
    94 
    95   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    96   {
    97     try { buffer.readLock(); body }
    98     finally { buffer.readUnlock() }
    99   }
   100 
   101   def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
   102   {
   103     try { buffer.beginCompoundEdit(); body }
   104     finally { buffer.endCompoundEdit() }
   105   }
   106 
   107 
   108   /* get text */
   109 
   110   def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
   111     try { Some(buffer.getText(range.start, range.length)) }
   112     catch { case _: ArrayIndexOutOfBoundsException => None }
   113 
   114 
   115   /* point range */
   116 
   117   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
   118     buffer_lock(buffer) {
   119       def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
   120       try {
   121         val c = text(offset)
   122         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
   123           Text.Range(offset, offset + 2)
   124         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
   125           Text.Range(offset - 1, offset + 1)
   126         else Text.Range(offset, offset + 1)
   127       }
   128       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
   129     }
   130 
   131 
   132   /* visible text range */
   133 
   134   def visible_range(text_area: TextArea): Option[Text.Range] =
   135   {
   136     val buffer = text_area.getBuffer
   137     val n = text_area.getVisibleLines
   138     if (n > 0) {
   139       val start = text_area.getScreenLineStartOffset(0)
   140       val raw_end = text_area.getScreenLineEndOffset(n - 1)
   141       val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
   142       Some(Text.Range(start, end))
   143     }
   144     else None
   145   }
   146 
   147   def invalidate_range(text_area: TextArea, range: Text.Range)
   148   {
   149     val buffer = text_area.getBuffer
   150     text_area.invalidateLineRange(
   151       buffer.getLineOfOffset(range.start),
   152       buffer.getLineOfOffset(range.stop))
   153   }
   154 
   155 
   156   /* char width */
   157 
   158   def char_width(text_area: TextArea): Int =
   159   {
   160     val painter = text_area.getPainter
   161     val font = painter.getFont
   162     val font_context = painter.getFontRenderContext
   163     font.getStringBounds(" ", font_context).getWidth.round.toInt
   164   }
   165 
   166 
   167   /* graphics range */
   168 
   169   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
   170 
   171   // NB: jEdit always normalizes \r\n and \r to \n
   172   // NB: last line lacks \n
   173   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   174   {
   175     val buffer = text_area.getBuffer
   176 
   177     val p = text_area.offsetToXY(range.start)
   178 
   179     val end = buffer.getLength
   180     val stop = range.stop
   181     val (q, r) =
   182       if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
   183       else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
   184         (text_area.offsetToXY(stop - 1), char_width(text_area))
   185       else (text_area.offsetToXY(stop), 0)
   186 
   187     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
   188       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
   189     else None
   190   }
   191 
   192 
   193   /* pixel range */
   194 
   195   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   196   {
   197     val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
   198     gfx_range(text_area, range) match {
   199       case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   200       case _ => None
   201     }
   202   }
   203 }
   204