src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Tue Aug 27 22:23:40 2013 +0200 (2013-08-27)
changeset 53237 6bfe54791591
parent 53231 423e29f1f304
child 53247 bd595338ca18
permissions -rw-r--r--
enable jEdit KeyEventWorkaround uniformly;
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@53226
    13
import java.awt.event.{KeyEvent, KeyListener}
wenzelm@53019
    14
import javax.swing.{Icon, ImageIcon, JWindow}
wenzelm@49710
    15
wenzelm@49710
    16
import scala.annotation.tailrec
wenzelm@49406
    17
wenzelm@52873
    18
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
wenzelm@53226
    19
import org.gjt.sp.jedit.gui.KeyEventWorkaround
wenzelm@49406
    20
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@51492
    21
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
wenzelm@49406
    22
wenzelm@49406
    23
wenzelm@49406
    24
object JEdit_Lib
wenzelm@49406
    25
{
wenzelm@50554
    26
  /* bounds within multi-screen environment */
wenzelm@50554
    27
wenzelm@50554
    28
  def screen_bounds(screen_point: Point): Rectangle =
wenzelm@50554
    29
  {
wenzelm@50554
    30
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
wenzelm@50554
    31
    (for {
wenzelm@50554
    32
      device <- ge.getScreenDevices.iterator
wenzelm@50554
    33
      config <- device.getConfigurations.iterator
wenzelm@50554
    34
      bounds = config.getBounds
wenzelm@50554
    35
    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
wenzelm@50554
    36
  }
wenzelm@50554
    37
wenzelm@50554
    38
wenzelm@53019
    39
  /* window geometry measurement */
wenzelm@53019
    40
wenzelm@53019
    41
  private lazy val dummy_window = new JWindow
wenzelm@53019
    42
wenzelm@53019
    43
  final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
wenzelm@53019
    44
  {
wenzelm@53019
    45
    def deco_width: Int = width - inner_width
wenzelm@53019
    46
    def deco_height: Int = height - inner_height
wenzelm@53019
    47
  }
wenzelm@53019
    48
wenzelm@53019
    49
  def window_geometry(outer: Container, inner: Component): Window_Geometry =
wenzelm@53019
    50
  {
wenzelm@53019
    51
    Swing_Thread.require()
wenzelm@53019
    52
wenzelm@53019
    53
    val old_content = dummy_window.getContentPane
wenzelm@53019
    54
wenzelm@53019
    55
    dummy_window.setContentPane(outer)
wenzelm@53019
    56
    dummy_window.pack
wenzelm@53019
    57
    dummy_window.revalidate
wenzelm@53019
    58
wenzelm@53019
    59
    val geometry =
wenzelm@53019
    60
      Window_Geometry(
wenzelm@53019
    61
        dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
wenzelm@53019
    62
wenzelm@53019
    63
    dummy_window.setContentPane(old_content)
wenzelm@53019
    64
wenzelm@53019
    65
    geometry
wenzelm@53019
    66
  }
wenzelm@53019
    67
wenzelm@53019
    68
wenzelm@49712
    69
  /* GUI components */
wenzelm@49712
    70
wenzelm@49712
    71
  def get_parent(component: Component): Option[Container] =
wenzelm@49712
    72
    component.getParent match {
wenzelm@49712
    73
      case null => None
wenzelm@49712
    74
      case parent => Some(parent)
wenzelm@49712
    75
    }
wenzelm@49712
    76
wenzelm@49712
    77
  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
wenzelm@49712
    78
    private var next_elem = get_parent(component)
wenzelm@49712
    79
    def hasNext(): Boolean = next_elem.isDefined
wenzelm@49712
    80
    def next(): Container =
wenzelm@49712
    81
      next_elem match {
wenzelm@49712
    82
        case Some(parent) =>
wenzelm@49712
    83
          next_elem = get_parent(parent)
wenzelm@49712
    84
          parent
wenzelm@49712
    85
        case None => Iterator.empty.next()
wenzelm@49712
    86
      }
wenzelm@49712
    87
  }
wenzelm@49712
    88
wenzelm@49712
    89
  def parent_window(component: Component): Option[Window] =
wenzelm@52478
    90
    ancestors(component).collectFirst({ case x: Window => x })
wenzelm@49710
    91
wenzelm@49710
    92
wenzelm@50186
    93
  /* basic tooltips, with multi-line support */
wenzelm@50186
    94
wenzelm@50186
    95
  def wrap_tooltip(text: String): String =
wenzelm@50186
    96
    if (text == "") null
wenzelm@50186
    97
    else "<html><pre>" + HTML.encode(text) + "</pre></html>"
wenzelm@50186
    98
wenzelm@50186
    99
wenzelm@49406
   100
  /* buffers */
wenzelm@49406
   101
wenzelm@49406
   102
  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@49406
   103
    Swing_Thread.now { buffer_lock(buffer) { body } }
wenzelm@49406
   104
wenzelm@49406
   105
  def buffer_text(buffer: JEditBuffer): String =
wenzelm@49406
   106
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
wenzelm@49406
   107
wenzelm@49406
   108
  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
wenzelm@49406
   109
wenzelm@49406
   110
wenzelm@49406
   111
  /* main jEdit components */
wenzelm@49406
   112
wenzelm@49406
   113
  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
wenzelm@49406
   114
wenzelm@49406
   115
  def jedit_buffer(name: String): Option[Buffer] =
wenzelm@49406
   116
    jedit_buffers().find(buffer => buffer_name(buffer) == name)
wenzelm@49406
   117
wenzelm@49406
   118
  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
wenzelm@49406
   119
wenzelm@49406
   120
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
wenzelm@49406
   121
    view.getEditPanes().iterator.map(_.getTextArea)
wenzelm@49406
   122
wenzelm@49406
   123
  def jedit_text_areas(): Iterator[JEditTextArea] =
wenzelm@49406
   124
    jedit_views().flatMap(jedit_text_areas(_))
wenzelm@49406
   125
wenzelm@49406
   126
  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
wenzelm@49406
   127
    jedit_text_areas().filter(_.getBuffer == buffer)
wenzelm@49406
   128
wenzelm@49406
   129
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@49406
   130
  {
wenzelm@49406
   131
    try { buffer.readLock(); body }
wenzelm@49406
   132
    finally { buffer.readUnlock() }
wenzelm@49406
   133
  }
wenzelm@49407
   134
wenzelm@50195
   135
  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@50195
   136
  {
wenzelm@50195
   137
    try { buffer.beginCompoundEdit(); body }
wenzelm@50195
   138
    finally { buffer.endCompoundEdit() }
wenzelm@50195
   139
  }
wenzelm@50195
   140
wenzelm@49407
   141
wenzelm@50215
   142
  /* get text */
wenzelm@50215
   143
wenzelm@50215
   144
  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
wenzelm@50215
   145
    try { Some(buffer.getText(range.start, range.length)) }
wenzelm@50215
   146
    catch { case _: ArrayIndexOutOfBoundsException => None }
wenzelm@50215
   147
wenzelm@50215
   148
wenzelm@50363
   149
  /* buffer range */
wenzelm@50363
   150
wenzelm@50363
   151
  def buffer_range(buffer: JEditBuffer): Text.Range =
wenzelm@50363
   152
    Text.Range(0, (buffer.getLength - 1) max 0)
wenzelm@50363
   153
wenzelm@50363
   154
wenzelm@49407
   155
  /* point range */
wenzelm@49407
   156
wenzelm@49407
   157
  def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
wenzelm@49407
   158
    buffer_lock(buffer) {
wenzelm@49407
   159
      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
wenzelm@49407
   160
      try {
wenzelm@49407
   161
        val c = text(offset)
wenzelm@49407
   162
        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
wenzelm@49407
   163
          Text.Range(offset, offset + 2)
wenzelm@49407
   164
        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
wenzelm@49407
   165
          Text.Range(offset - 1, offset + 1)
wenzelm@49407
   166
        else Text.Range(offset, offset + 1)
wenzelm@49407
   167
      }
wenzelm@49407
   168
      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
wenzelm@49407
   169
    }
wenzelm@49408
   170
wenzelm@49408
   171
wenzelm@49408
   172
  /* visible text range */
wenzelm@49408
   173
wenzelm@49408
   174
  def visible_range(text_area: TextArea): Option[Text.Range] =
wenzelm@49408
   175
  {
wenzelm@49408
   176
    val buffer = text_area.getBuffer
wenzelm@49408
   177
    val n = text_area.getVisibleLines
wenzelm@49408
   178
    if (n > 0) {
wenzelm@49408
   179
      val start = text_area.getScreenLineStartOffset(0)
wenzelm@49408
   180
      val raw_end = text_area.getScreenLineEndOffset(n - 1)
wenzelm@49843
   181
      val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
wenzelm@49843
   182
      Some(Text.Range(start, end))
wenzelm@49408
   183
    }
wenzelm@49408
   184
    else None
wenzelm@49408
   185
  }
wenzelm@49408
   186
wenzelm@49408
   187
  def invalidate_range(text_area: TextArea, range: Text.Range)
wenzelm@49408
   188
  {
wenzelm@49408
   189
    val buffer = text_area.getBuffer
wenzelm@49408
   190
    text_area.invalidateLineRange(
wenzelm@49408
   191
      buffer.getLineOfOffset(range.start),
wenzelm@49408
   192
      buffer.getLineOfOffset(range.stop))
wenzelm@49408
   193
  }
wenzelm@49409
   194
wenzelm@49409
   195
wenzelm@49409
   196
  /* graphics range */
wenzelm@49409
   197
wenzelm@50115
   198
  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
wenzelm@49409
   199
wenzelm@49843
   200
  // NB: jEdit always normalizes \r\n and \r to \n
wenzelm@49409
   201
  // NB: last line lacks \n
wenzelm@49409
   202
  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
wenzelm@49409
   203
  {
wenzelm@51507
   204
    val metric = pretty_metric(text_area.getPainter)
wenzelm@51492
   205
    val char_width = (metric.unit * metric.average).round.toInt
wenzelm@50849
   206
wenzelm@49409
   207
    val buffer = text_area.getBuffer
wenzelm@49409
   208
wenzelm@49409
   209
    val end = buffer.getLength
wenzelm@49409
   210
    val stop = range.stop
wenzelm@51078
   211
wenzelm@51078
   212
    val (p, q, r) =
wenzelm@51078
   213
      try {
wenzelm@51078
   214
        val p = text_area.offsetToXY(range.start)
wenzelm@51078
   215
        val (q, r) =
wenzelm@51078
   216
          if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
wenzelm@51078
   217
          else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
wenzelm@51078
   218
            (text_area.offsetToXY(stop - 1), char_width)
wenzelm@51078
   219
          else (text_area.offsetToXY(stop), 0)
wenzelm@51078
   220
        (p, q, r)
wenzelm@51078
   221
      }
wenzelm@51078
   222
      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
wenzelm@49409
   223
wenzelm@49409
   224
    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
wenzelm@50115
   225
      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
wenzelm@49409
   226
    else None
wenzelm@49409
   227
  }
wenzelm@49941
   228
wenzelm@49941
   229
wenzelm@49941
   230
  /* pixel range */
wenzelm@49941
   231
wenzelm@49941
   232
  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
wenzelm@49941
   233
  {
wenzelm@53183
   234
    // coordinates wrt. inner painter component
wenzelm@53183
   235
    val painter = text_area.getPainter
wenzelm@53183
   236
    if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
wenzelm@53183
   237
      val offset = text_area.xyToOffset(x, y, false)
wenzelm@53183
   238
      if (offset >= 0) {
wenzelm@53183
   239
        val range = point_range(text_area.getBuffer, offset)
wenzelm@53183
   240
        gfx_range(text_area, range) match {
wenzelm@53183
   241
          case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
wenzelm@53183
   242
          case _ => None
wenzelm@53183
   243
        }
wenzelm@53183
   244
      }
wenzelm@53183
   245
      else None
wenzelm@49941
   246
    }
wenzelm@53183
   247
    else None
wenzelm@49941
   248
  }
wenzelm@51492
   249
wenzelm@51492
   250
wenzelm@51492
   251
  /* pretty text metric */
wenzelm@51492
   252
wenzelm@51507
   253
  abstract class Pretty_Metric extends Pretty.Metric
wenzelm@51507
   254
  {
wenzelm@51507
   255
    def average: Double
wenzelm@51507
   256
  }
wenzelm@51492
   257
wenzelm@51507
   258
  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
wenzelm@51507
   259
    new Pretty_Metric {
wenzelm@51507
   260
      def string_width(s: String): Double =
wenzelm@51507
   261
        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
wenzelm@51507
   262
wenzelm@51507
   263
      val unit = string_width(Pretty.space)
wenzelm@51507
   264
      val average = string_width("mix") / (3 * unit)
wenzelm@51507
   265
      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
wenzelm@51492
   266
    }
wenzelm@52873
   267
wenzelm@52873
   268
wenzelm@52873
   269
  /* icons */
wenzelm@52873
   270
wenzelm@52873
   271
  def load_icon(name: String): Icon =
wenzelm@52873
   272
  {
wenzelm@52873
   273
    val name1 =
wenzelm@52873
   274
      if (name.startsWith("idea-icons/")) {
wenzelm@52873
   275
        val file =
wenzelm@52873
   276
          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
wenzelm@52873
   277
        "jar:" + file + "!/" + name
wenzelm@52873
   278
      }
wenzelm@52873
   279
      else name
wenzelm@52873
   280
    val icon = GUIUtilities.loadIcon(name1)
wenzelm@52873
   281
    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
wenzelm@52873
   282
    else icon
wenzelm@52873
   283
  }
wenzelm@52874
   284
wenzelm@52874
   285
  def load_image_icon(name: String): ImageIcon =
wenzelm@52874
   286
    load_icon(name) match {
wenzelm@52874
   287
      case icon: ImageIcon => icon
wenzelm@52874
   288
      case _ => error("Bad image icon: " + name)
wenzelm@52874
   289
    }
wenzelm@53226
   290
wenzelm@53226
   291
wenzelm@53231
   292
  /* key event handling */
wenzelm@53231
   293
wenzelm@53231
   294
  def request_focus_view
wenzelm@53231
   295
  {
wenzelm@53231
   296
    val view = jEdit.getActiveView()
wenzelm@53231
   297
    if (view != null) {
wenzelm@53231
   298
      val text_area = view.getTextArea
wenzelm@53231
   299
      if (text_area != null) text_area.requestFocus
wenzelm@53231
   300
    }
wenzelm@53231
   301
  }
wenzelm@53231
   302
wenzelm@53231
   303
  def propagate_key(view: View, evt: KeyEvent)
wenzelm@53231
   304
  {
wenzelm@53231
   305
    if (view != null && !evt.isConsumed)
wenzelm@53231
   306
      view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
wenzelm@53231
   307
  }
wenzelm@53226
   308
wenzelm@53226
   309
  def key_listener(
wenzelm@53226
   310
    key_typed: KeyEvent => Unit = _ => (),
wenzelm@53226
   311
    key_pressed: KeyEvent => Unit = _ => (),
wenzelm@53226
   312
    key_released: KeyEvent => Unit = _ => ()): KeyListener =
wenzelm@53226
   313
  {
wenzelm@53226
   314
    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
wenzelm@53226
   315
    {
wenzelm@53237
   316
      val evt = KeyEventWorkaround.processKeyEvent(evt0)
wenzelm@53226
   317
      if (evt != null) handle(evt)
wenzelm@53226
   318
    }
wenzelm@53226
   319
wenzelm@53226
   320
    new KeyListener
wenzelm@53226
   321
    {
wenzelm@53226
   322
      def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
wenzelm@53226
   323
      def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
wenzelm@53226
   324
      def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
wenzelm@53226
   325
    }
wenzelm@53226
   326
  }
wenzelm@49406
   327
}
wenzelm@49406
   328