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