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