src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Fri Oct 05 13:48:22 2012 +0200 (2012-10-05)
changeset 49710 21d88a631fcc
parent 49409 7140a738aa49
child 49712 a1bd8fe5131b
permissions -rw-r--r--
refer to parent frame -- relevant for floating dockables in particular;
     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}
    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   /* frames */
    24 
    25   def parent_frame(component: Component): Option[Frame] =
    26   {
    27     @tailrec def find(c: Container): Option[Frame] =
    28       c match {
    29         case null => None
    30         case frame: Frame => Some(frame)
    31         case _ => find(c.getParent)
    32       }
    33     find(component.getParent)
    34   }
    35 
    36 
    37   /* buffers */
    38 
    39   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    40     Swing_Thread.now { buffer_lock(buffer) { body } }
    41 
    42   def buffer_text(buffer: JEditBuffer): String =
    43     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    44 
    45   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    46 
    47   def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
    48     Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
    49 
    50   def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    51   {
    52     val name = buffer_name(buffer)
    53     Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    54   }
    55 
    56 
    57   /* main jEdit components */
    58 
    59   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    60 
    61   def jedit_buffer(name: String): Option[Buffer] =
    62     jedit_buffers().find(buffer => buffer_name(buffer) == name)
    63 
    64   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    65 
    66   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    67     view.getEditPanes().iterator.map(_.getTextArea)
    68 
    69   def jedit_text_areas(): Iterator[JEditTextArea] =
    70     jedit_views().flatMap(jedit_text_areas(_))
    71 
    72   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
    73     jedit_text_areas().filter(_.getBuffer == buffer)
    74 
    75   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    76   {
    77     try { buffer.readLock(); body }
    78     finally { buffer.readUnlock() }
    79   }
    80 
    81 
    82   /* point range */
    83 
    84   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
    85     buffer_lock(buffer) {
    86       def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
    87       try {
    88         val c = text(offset)
    89         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
    90           Text.Range(offset, offset + 2)
    91         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
    92           Text.Range(offset - 1, offset + 1)
    93         else Text.Range(offset, offset + 1)
    94       }
    95       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
    96     }
    97 
    98 
    99   /* proper line range */
   100 
   101   // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
   102   def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range =
   103     Text.Range(start, end min buffer.getLength)
   104 
   105 
   106   /* visible text range */
   107 
   108   def visible_range(text_area: TextArea): Option[Text.Range] =
   109   {
   110     val buffer = text_area.getBuffer
   111     val n = text_area.getVisibleLines
   112     if (n > 0) {
   113       val start = text_area.getScreenLineStartOffset(0)
   114       val raw_end = text_area.getScreenLineEndOffset(n - 1)
   115       Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength))
   116     }
   117     else None
   118   }
   119 
   120   def invalidate_range(text_area: TextArea, range: Text.Range)
   121   {
   122     val buffer = text_area.getBuffer
   123     text_area.invalidateLineRange(
   124       buffer.getLineOfOffset(range.start),
   125       buffer.getLineOfOffset(range.stop))
   126   }
   127 
   128 
   129   /* char width */
   130 
   131   def char_width(text_area: TextArea): Int =
   132   {
   133     val painter = text_area.getPainter
   134     val font = painter.getFont
   135     val font_context = painter.getFontRenderContext
   136     font.getStringBounds(" ", font_context).getWidth.round.toInt
   137   }
   138 
   139 
   140   /* graphics range */
   141 
   142   class Gfx_Range(val x: Int, val y: Int, val length: Int)
   143 
   144   // NB: jEdit already normalizes \r\n and \r to \n
   145   // NB: last line lacks \n
   146   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   147   {
   148     val buffer = text_area.getBuffer
   149 
   150     val p = text_area.offsetToXY(range.start)
   151 
   152     val end = buffer.getLength
   153     val stop = range.stop
   154     val (q, r) =
   155       if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
   156       else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
   157         (text_area.offsetToXY(stop - 1), char_width(text_area))
   158       else (text_area.offsetToXY(stop), 0)
   159 
   160     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
   161       Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
   162     else None
   163   }
   164 }
   165