src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Tue Aug 13 13:18:26 2013 +0200 (2013-08-13)
changeset 53003 39da27fc6101
parent 52874 91032244e4ca
child 53019 be9e94594b96
permissions -rw-r--r--
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
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@50658
    12
import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
wenzelm@52874
    13
import javax.swing.{Icon, ImageIcon}
wenzelm@49710
    14
wenzelm@49710
    15
import scala.annotation.tailrec
wenzelm@49406
    16
wenzelm@52873
    17
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
wenzelm@49406
    18
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@51492
    19
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
wenzelm@49406
    20
wenzelm@49406
    21
wenzelm@49406
    22
object JEdit_Lib
wenzelm@49406
    23
{
wenzelm@50554
    24
  /* bounds within multi-screen environment */
wenzelm@50554
    25
wenzelm@50554
    26
  def screen_bounds(screen_point: Point): Rectangle =
wenzelm@50554
    27
  {
wenzelm@50554
    28
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
wenzelm@50554
    29
    (for {
wenzelm@50554
    30
      device <- ge.getScreenDevices.iterator
wenzelm@50554
    31
      config <- device.getConfigurations.iterator
wenzelm@50554
    32
      bounds = config.getBounds
wenzelm@50554
    33
    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
wenzelm@50554
    34
  }
wenzelm@50554
    35
wenzelm@50554
    36
wenzelm@49712
    37
  /* GUI components */
wenzelm@49712
    38
wenzelm@49712
    39
  def get_parent(component: Component): Option[Container] =
wenzelm@49712
    40
    component.getParent match {
wenzelm@49712
    41
      case null => None
wenzelm@49712
    42
      case parent => Some(parent)
wenzelm@49712
    43
    }
wenzelm@49712
    44
wenzelm@49712
    45
  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
wenzelm@49712
    46
    private var next_elem = get_parent(component)
wenzelm@49712
    47
    def hasNext(): Boolean = next_elem.isDefined
wenzelm@49712
    48
    def next(): Container =
wenzelm@49712
    49
      next_elem match {
wenzelm@49712
    50
        case Some(parent) =>
wenzelm@49712
    51
          next_elem = get_parent(parent)
wenzelm@49712
    52
          parent
wenzelm@49712
    53
        case None => Iterator.empty.next()
wenzelm@49712
    54
      }
wenzelm@49712
    55
  }
wenzelm@49712
    56
wenzelm@49712
    57
  def parent_window(component: Component): Option[Window] =
wenzelm@52478
    58
    ancestors(component).collectFirst({ case x: Window => x })
wenzelm@49710
    59
wenzelm@49710
    60
wenzelm@50186
    61
  /* basic tooltips, with multi-line support */
wenzelm@50186
    62
wenzelm@50186
    63
  def wrap_tooltip(text: String): String =
wenzelm@50186
    64
    if (text == "") null
wenzelm@50186
    65
    else "<html><pre>" + HTML.encode(text) + "</pre></html>"
wenzelm@50186
    66
wenzelm@50186
    67
wenzelm@49406
    68
  /* buffers */
wenzelm@49406
    69
wenzelm@49406
    70
  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@49406
    71
    Swing_Thread.now { buffer_lock(buffer) { body } }
wenzelm@49406
    72
wenzelm@49406
    73
  def buffer_text(buffer: JEditBuffer): String =
wenzelm@49406
    74
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
wenzelm@49406
    75
wenzelm@49406
    76
  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
wenzelm@49406
    77
wenzelm@49406
    78
wenzelm@53003
    79
  /* focus of main window */
wenzelm@53003
    80
wenzelm@53003
    81
  def request_focus_view: Unit =
wenzelm@53003
    82
  {
wenzelm@53003
    83
    jEdit.getActiveView() match {
wenzelm@53003
    84
      case null =>
wenzelm@53003
    85
      case view =>
wenzelm@53003
    86
        view.getTextArea match {
wenzelm@53003
    87
          case null =>
wenzelm@53003
    88
          case text_area => text_area.requestFocus
wenzelm@53003
    89
        }
wenzelm@53003
    90
    }
wenzelm@53003
    91
  }
wenzelm@53003
    92
wenzelm@53003
    93
wenzelm@49406
    94
  /* main jEdit components */
wenzelm@49406
    95
wenzelm@49406
    96
  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
wenzelm@49406
    97
wenzelm@49406
    98
  def jedit_buffer(name: String): Option[Buffer] =
wenzelm@49406
    99
    jedit_buffers().find(buffer => buffer_name(buffer) == name)
wenzelm@49406
   100
wenzelm@49406
   101
  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
wenzelm@49406
   102
wenzelm@49406
   103
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
wenzelm@49406
   104
    view.getEditPanes().iterator.map(_.getTextArea)
wenzelm@49406
   105
wenzelm@49406
   106
  def jedit_text_areas(): Iterator[JEditTextArea] =
wenzelm@49406
   107
    jedit_views().flatMap(jedit_text_areas(_))
wenzelm@49406
   108
wenzelm@49406
   109
  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
wenzelm@49406
   110
    jedit_text_areas().filter(_.getBuffer == buffer)
wenzelm@49406
   111
wenzelm@49406
   112
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@49406
   113
  {
wenzelm@49406
   114
    try { buffer.readLock(); body }
wenzelm@49406
   115
    finally { buffer.readUnlock() }
wenzelm@49406
   116
  }
wenzelm@49407
   117
wenzelm@50195
   118
  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@50195
   119
  {
wenzelm@50195
   120
    try { buffer.beginCompoundEdit(); body }
wenzelm@50195
   121
    finally { buffer.endCompoundEdit() }
wenzelm@50195
   122
  }
wenzelm@50195
   123
wenzelm@49407
   124
wenzelm@50215
   125
  /* get text */
wenzelm@50215
   126
wenzelm@50215
   127
  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
wenzelm@50215
   128
    try { Some(buffer.getText(range.start, range.length)) }
wenzelm@50215
   129
    catch { case _: ArrayIndexOutOfBoundsException => None }
wenzelm@50215
   130
wenzelm@50215
   131
wenzelm@50363
   132
  /* buffer range */
wenzelm@50363
   133
wenzelm@50363
   134
  def buffer_range(buffer: JEditBuffer): Text.Range =
wenzelm@50363
   135
    Text.Range(0, (buffer.getLength - 1) max 0)
wenzelm@50363
   136
wenzelm@50363
   137
wenzelm@49407
   138
  /* point range */
wenzelm@49407
   139
wenzelm@49407
   140
  def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
wenzelm@49407
   141
    buffer_lock(buffer) {
wenzelm@49407
   142
      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
wenzelm@49407
   143
      try {
wenzelm@49407
   144
        val c = text(offset)
wenzelm@49407
   145
        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
wenzelm@49407
   146
          Text.Range(offset, offset + 2)
wenzelm@49407
   147
        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
wenzelm@49407
   148
          Text.Range(offset - 1, offset + 1)
wenzelm@49407
   149
        else Text.Range(offset, offset + 1)
wenzelm@49407
   150
      }
wenzelm@49407
   151
      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
wenzelm@49407
   152
    }
wenzelm@49408
   153
wenzelm@49408
   154
wenzelm@49408
   155
  /* visible text range */
wenzelm@49408
   156
wenzelm@49408
   157
  def visible_range(text_area: TextArea): Option[Text.Range] =
wenzelm@49408
   158
  {
wenzelm@49408
   159
    val buffer = text_area.getBuffer
wenzelm@49408
   160
    val n = text_area.getVisibleLines
wenzelm@49408
   161
    if (n > 0) {
wenzelm@49408
   162
      val start = text_area.getScreenLineStartOffset(0)
wenzelm@49408
   163
      val raw_end = text_area.getScreenLineEndOffset(n - 1)
wenzelm@49843
   164
      val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
wenzelm@49843
   165
      Some(Text.Range(start, end))
wenzelm@49408
   166
    }
wenzelm@49408
   167
    else None
wenzelm@49408
   168
  }
wenzelm@49408
   169
wenzelm@49408
   170
  def invalidate_range(text_area: TextArea, range: Text.Range)
wenzelm@49408
   171
  {
wenzelm@49408
   172
    val buffer = text_area.getBuffer
wenzelm@49408
   173
    text_area.invalidateLineRange(
wenzelm@49408
   174
      buffer.getLineOfOffset(range.start),
wenzelm@49408
   175
      buffer.getLineOfOffset(range.stop))
wenzelm@49408
   176
  }
wenzelm@49409
   177
wenzelm@49409
   178
wenzelm@49409
   179
  /* graphics range */
wenzelm@49409
   180
wenzelm@50115
   181
  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
wenzelm@49409
   182
wenzelm@49843
   183
  // NB: jEdit always normalizes \r\n and \r to \n
wenzelm@49409
   184
  // NB: last line lacks \n
wenzelm@49409
   185
  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
wenzelm@49409
   186
  {
wenzelm@51507
   187
    val metric = pretty_metric(text_area.getPainter)
wenzelm@51492
   188
    val char_width = (metric.unit * metric.average).round.toInt
wenzelm@50849
   189
wenzelm@49409
   190
    val buffer = text_area.getBuffer
wenzelm@49409
   191
wenzelm@49409
   192
    val end = buffer.getLength
wenzelm@49409
   193
    val stop = range.stop
wenzelm@51078
   194
wenzelm@51078
   195
    val (p, q, r) =
wenzelm@51078
   196
      try {
wenzelm@51078
   197
        val p = text_area.offsetToXY(range.start)
wenzelm@51078
   198
        val (q, r) =
wenzelm@51078
   199
          if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
wenzelm@51078
   200
          else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
wenzelm@51078
   201
            (text_area.offsetToXY(stop - 1), char_width)
wenzelm@51078
   202
          else (text_area.offsetToXY(stop), 0)
wenzelm@51078
   203
        (p, q, r)
wenzelm@51078
   204
      }
wenzelm@51078
   205
      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
wenzelm@49409
   206
wenzelm@49409
   207
    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
wenzelm@50115
   208
      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
wenzelm@49409
   209
    else None
wenzelm@49409
   210
  }
wenzelm@49941
   211
wenzelm@49941
   212
wenzelm@49941
   213
  /* pixel range */
wenzelm@49941
   214
wenzelm@49941
   215
  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
wenzelm@49941
   216
  {
wenzelm@50116
   217
    val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
wenzelm@49941
   218
    gfx_range(text_area, range) match {
wenzelm@49941
   219
      case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
wenzelm@49941
   220
      case _ => None
wenzelm@49941
   221
    }
wenzelm@49941
   222
  }
wenzelm@51492
   223
wenzelm@51492
   224
wenzelm@51492
   225
  /* pretty text metric */
wenzelm@51492
   226
wenzelm@51507
   227
  abstract class Pretty_Metric extends Pretty.Metric
wenzelm@51507
   228
  {
wenzelm@51507
   229
    def average: Double
wenzelm@51507
   230
  }
wenzelm@51492
   231
wenzelm@51507
   232
  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
wenzelm@51507
   233
    new Pretty_Metric {
wenzelm@51507
   234
      def string_width(s: String): Double =
wenzelm@51507
   235
        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
wenzelm@51507
   236
wenzelm@51507
   237
      val unit = string_width(Pretty.space)
wenzelm@51507
   238
      val average = string_width("mix") / (3 * unit)
wenzelm@51507
   239
      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
wenzelm@51492
   240
    }
wenzelm@52873
   241
wenzelm@52873
   242
wenzelm@52873
   243
  /* icons */
wenzelm@52873
   244
wenzelm@52873
   245
  def load_icon(name: String): Icon =
wenzelm@52873
   246
  {
wenzelm@52873
   247
    val name1 =
wenzelm@52873
   248
      if (name.startsWith("idea-icons/")) {
wenzelm@52873
   249
        val file =
wenzelm@52873
   250
          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
wenzelm@52873
   251
        "jar:" + file + "!/" + name
wenzelm@52873
   252
      }
wenzelm@52873
   253
      else name
wenzelm@52873
   254
    val icon = GUIUtilities.loadIcon(name1)
wenzelm@52873
   255
    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
wenzelm@52873
   256
    else icon
wenzelm@52873
   257
  }
wenzelm@52874
   258
wenzelm@52874
   259
  def load_image_icon(name: String): ImageIcon =
wenzelm@52874
   260
    load_icon(name) match {
wenzelm@52874
   261
      case icon: ImageIcon => icon
wenzelm@52874
   262
      case _ => error("Bad image icon: " + name)
wenzelm@52874
   263
    }
wenzelm@49406
   264
}
wenzelm@49406
   265