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