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