src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Thu Apr 14 22:55:53 2016 +0200 (2016-04-14)
changeset 62986 9d2fae6b31cc
parent 62264 340f98836fd9
child 63426 2e4de628201f
permissions -rw-r--r--
background color for entity def/ref focus;
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@53712
    12
import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
wenzelm@53784
    13
import java.awt.event.{InputEvent, KeyEvent, KeyListener}
wenzelm@53247
    14
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
wenzelm@49710
    15
wenzelm@49710
    16
import scala.annotation.tailrec
wenzelm@56823
    17
import scala.util.parsing.input.CharSequenceReader
wenzelm@49406
    18
wenzelm@62264
    19
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
wenzelm@53226
    20
import org.gjt.sp.jedit.gui.KeyEventWorkaround
wenzelm@61192
    21
import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
wenzelm@51492
    22
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
wenzelm@59076
    23
import org.gjt.sp.jedit.syntax.TokenMarker
wenzelm@49406
    24
wenzelm@49406
    25
wenzelm@49406
    26
object JEdit_Lib
wenzelm@49406
    27
{
wenzelm@53247
    28
  /* location within multi-screen environment */
wenzelm@53247
    29
wenzelm@53247
    30
  final case class Screen_Location(point: Point, bounds: Rectangle)
wenzelm@53247
    31
  {
wenzelm@53247
    32
    def relative(parent: Component, size: Dimension): Point =
wenzelm@53247
    33
    {
wenzelm@53247
    34
      val w = size.width
wenzelm@53247
    35
      val h = size.height
wenzelm@50554
    36
wenzelm@53247
    37
      val x0 = parent.getLocationOnScreen.x
wenzelm@53247
    38
      val y0 = parent.getLocationOnScreen.y
wenzelm@53247
    39
      val x1 = x0 + parent.getWidth - w
wenzelm@53247
    40
      val y1 = y0 + parent.getHeight - h
wenzelm@53247
    41
      val x2 = point.x min (bounds.x + bounds.width - w)
wenzelm@53247
    42
      val y2 = point.y min (bounds.y + bounds.height - h)
wenzelm@53247
    43
wenzelm@53247
    44
      val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
wenzelm@53247
    45
      SwingUtilities.convertPointFromScreen(location, parent)
wenzelm@53247
    46
      location
wenzelm@53247
    47
    }
wenzelm@53247
    48
  }
wenzelm@53247
    49
wenzelm@53247
    50
  def screen_location(component: Component, point: Point): Screen_Location =
wenzelm@50554
    51
  {
wenzelm@53247
    52
    val screen_point = new Point(point.x, point.y)
wenzelm@53247
    53
    SwingUtilities.convertPointToScreen(screen_point, component)
wenzelm@53247
    54
wenzelm@50554
    55
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
wenzelm@53247
    56
    val screen_bounds =
wenzelm@53247
    57
      (for {
wenzelm@53247
    58
        device <- ge.getScreenDevices.iterator
wenzelm@53247
    59
        config <- device.getConfigurations.iterator
wenzelm@53247
    60
        bounds = config.getBounds
wenzelm@53247
    61
      } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
wenzelm@53247
    62
wenzelm@53247
    63
    Screen_Location(screen_point, screen_bounds)
wenzelm@50554
    64
  }
wenzelm@50554
    65
wenzelm@50554
    66
wenzelm@53019
    67
  /* window geometry measurement */
wenzelm@53019
    68
wenzelm@53019
    69
  private lazy val dummy_window = new JWindow
wenzelm@53019
    70
wenzelm@53019
    71
  final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
wenzelm@53019
    72
  {
wenzelm@53019
    73
    def deco_width: Int = width - inner_width
wenzelm@53019
    74
    def deco_height: Int = height - inner_height
wenzelm@53019
    75
  }
wenzelm@53019
    76
wenzelm@53019
    77
  def window_geometry(outer: Container, inner: Component): Window_Geometry =
wenzelm@53019
    78
  {
wenzelm@57612
    79
    GUI_Thread.require {}
wenzelm@53019
    80
wenzelm@53019
    81
    val old_content = dummy_window.getContentPane
wenzelm@53019
    82
wenzelm@53019
    83
    dummy_window.setContentPane(outer)
wenzelm@53019
    84
    dummy_window.pack
wenzelm@53019
    85
    dummy_window.revalidate
wenzelm@53019
    86
wenzelm@53019
    87
    val geometry =
wenzelm@53019
    88
      Window_Geometry(
wenzelm@53019
    89
        dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
wenzelm@53019
    90
wenzelm@53019
    91
    dummy_window.setContentPane(old_content)
wenzelm@53019
    92
wenzelm@53019
    93
    geometry
wenzelm@53019
    94
  }
wenzelm@53019
    95
wenzelm@53019
    96
wenzelm@49406
    97
  /* buffers */
wenzelm@49406
    98
wenzelm@49406
    99
  def buffer_text(buffer: JEditBuffer): String =
wenzelm@49406
   100
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
wenzelm@49406
   101
wenzelm@56823
   102
  def buffer_reader(buffer: JEditBuffer): CharSequenceReader =
wenzelm@56823
   103
    new CharSequenceReader(buffer.getSegment(0, buffer.getLength))
wenzelm@56823
   104
wenzelm@53274
   105
  def buffer_mode(buffer: JEditBuffer): String =
wenzelm@53274
   106
  {
wenzelm@53274
   107
    val mode = buffer.getMode
wenzelm@53274
   108
    if (mode == null) ""
wenzelm@53274
   109
    else {
wenzelm@53274
   110
      val name = mode.getName
wenzelm@53274
   111
      if (name == null) "" else name
wenzelm@53274
   112
    }
wenzelm@53274
   113
  }
wenzelm@53274
   114
wenzelm@49406
   115
  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
wenzelm@49406
   116
wenzelm@61192
   117
  def buffer_line_manager(buffer: JEditBuffer): LineManager =
wenzelm@61192
   118
    Untyped.get[LineManager](buffer, "lineMgr")
wenzelm@61192
   119
wenzelm@49406
   120
wenzelm@49406
   121
  /* main jEdit components */
wenzelm@49406
   122
wenzelm@49406
   123
  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
wenzelm@49406
   124
wenzelm@49406
   125
  def jedit_buffer(name: String): Option[Buffer] =
wenzelm@49406
   126
    jedit_buffers().find(buffer => buffer_name(buffer) == name)
wenzelm@49406
   127
wenzelm@56457
   128
  def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
wenzelm@56457
   129
    jedit_buffer(name.node)
wenzelm@56457
   130
wenzelm@49406
   131
  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
wenzelm@49406
   132
wenzelm@62264
   133
  def jedit_edit_panes(view: View): Iterator[EditPane] =
wenzelm@62264
   134
    if (view == null) Iterator.empty
wenzelm@62264
   135
    else view.getEditPanes().iterator.filter(_ != null)
wenzelm@62264
   136
wenzelm@49406
   137
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
wenzelm@56587
   138
    if (view == null) Iterator.empty
wenzelm@56587
   139
    else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
wenzelm@49406
   140
wenzelm@49406
   141
  def jedit_text_areas(): Iterator[JEditTextArea] =
wenzelm@49406
   142
    jedit_views().flatMap(jedit_text_areas(_))
wenzelm@49406
   143
wenzelm@49406
   144
  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
wenzelm@49406
   145
    jedit_text_areas().filter(_.getBuffer == buffer)
wenzelm@49406
   146
wenzelm@49406
   147
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@49406
   148
  {
wenzelm@49406
   149
    try { buffer.readLock(); body }
wenzelm@49406
   150
    finally { buffer.readUnlock() }
wenzelm@49406
   151
  }
wenzelm@49407
   152
wenzelm@50195
   153
  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@50195
   154
  {
wenzelm@50195
   155
    try { buffer.beginCompoundEdit(); body }
wenzelm@50195
   156
    finally { buffer.endCompoundEdit() }
wenzelm@50195
   157
  }
wenzelm@50195
   158
wenzelm@49407
   159
wenzelm@50215
   160
  /* get text */
wenzelm@50215
   161
wenzelm@50215
   162
  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
wenzelm@50215
   163
    try { Some(buffer.getText(range.start, range.length)) }
wenzelm@50215
   164
    catch { case _: ArrayIndexOutOfBoundsException => None }
wenzelm@50215
   165
wenzelm@53784
   166
  def try_get_text(text: String, range: Text.Range): Option[String] =
wenzelm@53784
   167
    try { Some(text.substring(range.start, range.stop)) }
wenzelm@53784
   168
    catch { case _: IndexOutOfBoundsException => None }
wenzelm@53784
   169
wenzelm@50215
   170
wenzelm@49407
   171
  /* point range */
wenzelm@49407
   172
wenzelm@49407
   173
  def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
wenzelm@56592
   174
    if (offset < 0) Text.Range.offside
wenzelm@56592
   175
    else
wenzelm@56592
   176
      buffer_lock(buffer) {
wenzelm@56592
   177
        def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
wenzelm@56592
   178
        try {
wenzelm@56592
   179
          val c = text(offset)
wenzelm@56592
   180
          if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
wenzelm@56592
   181
            Text.Range(offset, offset + 2)
wenzelm@56592
   182
          else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
wenzelm@56592
   183
            Text.Range(offset - 1, offset + 1)
wenzelm@56592
   184
          else
wenzelm@56592
   185
            Text.Range(offset, offset + 1)
wenzelm@56592
   186
        }
wenzelm@56592
   187
        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
wenzelm@49407
   188
      }
wenzelm@49408
   189
wenzelm@49408
   190
wenzelm@55812
   191
  /* text ranges */
wenzelm@55812
   192
wenzelm@55812
   193
  def buffer_range(buffer: JEditBuffer): Text.Range =
wenzelm@55812
   194
    Text.Range(0, buffer.getLength)
wenzelm@49408
   195
wenzelm@56587
   196
  def line_range(buffer: JEditBuffer, line: Int): Text.Range =
wenzelm@56589
   197
    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
wenzelm@56587
   198
wenzelm@56592
   199
  def caret_range(text_area: TextArea): Text.Range =
wenzelm@56592
   200
    point_range(text_area.getBuffer, text_area.getCaretPosition)
wenzelm@56592
   201
wenzelm@56593
   202
  def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
wenzelm@56587
   203
  {
wenzelm@56587
   204
    val snapshot = rendering.snapshot
wenzelm@56587
   205
    val former_caret = snapshot.revert(text_area.getCaretPosition)
wenzelm@56593
   206
    snapshot.convert(Text.Range(former_caret - 1, former_caret))
wenzelm@56587
   207
  }
wenzelm@56587
   208
wenzelm@49408
   209
  def visible_range(text_area: TextArea): Option[Text.Range] =
wenzelm@49408
   210
  {
wenzelm@49408
   211
    val buffer = text_area.getBuffer
wenzelm@49408
   212
    val n = text_area.getVisibleLines
wenzelm@49408
   213
    if (n > 0) {
wenzelm@49408
   214
      val start = text_area.getScreenLineStartOffset(0)
wenzelm@49408
   215
      val raw_end = text_area.getScreenLineEndOffset(n - 1)
wenzelm@49843
   216
      val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
wenzelm@49843
   217
      Some(Text.Range(start, end))
wenzelm@49408
   218
    }
wenzelm@49408
   219
    else None
wenzelm@49408
   220
  }
wenzelm@49408
   221
wenzelm@49408
   222
  def invalidate_range(text_area: TextArea, range: Text.Range)
wenzelm@49408
   223
  {
wenzelm@49408
   224
    val buffer = text_area.getBuffer
wenzelm@55812
   225
    buffer_range(buffer).try_restrict(range) match {
wenzelm@55812
   226
      case Some(range1) if !range1.is_singularity =>
wenzelm@56699
   227
        try {
wenzelm@56699
   228
          text_area.invalidateLineRange(
wenzelm@56699
   229
            buffer.getLineOfOffset(range1.start),
wenzelm@56699
   230
            buffer.getLineOfOffset(range1.stop))
wenzelm@56699
   231
        }
wenzelm@56699
   232
        catch { case _: ArrayIndexOutOfBoundsException => }
wenzelm@55812
   233
      case _ =>
wenzelm@55812
   234
    }
wenzelm@49408
   235
  }
wenzelm@49409
   236
wenzelm@62986
   237
  def invalidate(text_area: TextArea)
wenzelm@62986
   238
  {
wenzelm@62986
   239
    val visible_lines = text_area.getVisibleLines
wenzelm@62986
   240
    if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
wenzelm@62986
   241
  }
wenzelm@62986
   242
wenzelm@49409
   243
wenzelm@49409
   244
  /* graphics range */
wenzelm@49409
   245
wenzelm@60215
   246
  case class Gfx_Range(x: Int, y: Int, length: Int)
wenzelm@49409
   247
wenzelm@49843
   248
  // NB: jEdit always normalizes \r\n and \r to \n
wenzelm@49409
   249
  // NB: last line lacks \n
wenzelm@49409
   250
  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
wenzelm@49409
   251
  {
wenzelm@51507
   252
    val metric = pretty_metric(text_area.getPainter)
wenzelm@51492
   253
    val char_width = (metric.unit * metric.average).round.toInt
wenzelm@50849
   254
wenzelm@49409
   255
    val buffer = text_area.getBuffer
wenzelm@49409
   256
wenzelm@49409
   257
    val end = buffer.getLength
wenzelm@49409
   258
    val stop = range.stop
wenzelm@51078
   259
wenzelm@51078
   260
    val (p, q, r) =
wenzelm@51078
   261
      try {
wenzelm@51078
   262
        val p = text_area.offsetToXY(range.start)
wenzelm@51078
   263
        val (q, r) =
wenzelm@55549
   264
          if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
wenzelm@51078
   265
            (text_area.offsetToXY(stop - 1), char_width)
wenzelm@55549
   266
          else if (stop >= end)
wenzelm@55549
   267
            (text_area.offsetToXY(end), char_width * (stop - end))
wenzelm@51078
   268
          else (text_area.offsetToXY(stop), 0)
wenzelm@51078
   269
        (p, q, r)
wenzelm@51078
   270
      }
wenzelm@51078
   271
      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
wenzelm@49409
   272
wenzelm@49409
   273
    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
wenzelm@50115
   274
      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
wenzelm@49409
   275
    else None
wenzelm@49409
   276
  }
wenzelm@49941
   277
wenzelm@49941
   278
wenzelm@49941
   279
  /* pixel range */
wenzelm@49941
   280
wenzelm@49941
   281
  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
wenzelm@49941
   282
  {
wenzelm@53183
   283
    // coordinates wrt. inner painter component
wenzelm@53183
   284
    val painter = text_area.getPainter
wenzelm@53183
   285
    if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
wenzelm@53183
   286
      val offset = text_area.xyToOffset(x, y, false)
wenzelm@53183
   287
      if (offset >= 0) {
wenzelm@53183
   288
        val range = point_range(text_area.getBuffer, offset)
wenzelm@53183
   289
        gfx_range(text_area, range) match {
wenzelm@60215
   290
          case Some(g) if g.x <= x && x < g.x + g.length => Some(range)
wenzelm@53183
   291
          case _ => None
wenzelm@53183
   292
        }
wenzelm@53183
   293
      }
wenzelm@53183
   294
      else None
wenzelm@49941
   295
    }
wenzelm@53183
   296
    else None
wenzelm@49941
   297
  }
wenzelm@51492
   298
wenzelm@51492
   299
wenzelm@51492
   300
  /* pretty text metric */
wenzelm@51492
   301
wenzelm@51507
   302
  abstract class Pretty_Metric extends Pretty.Metric
wenzelm@51507
   303
  {
wenzelm@51507
   304
    def average: Double
wenzelm@51507
   305
  }
wenzelm@51492
   306
wenzelm@51507
   307
  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
wenzelm@51507
   308
    new Pretty_Metric {
wenzelm@51507
   309
      def string_width(s: String): Double =
wenzelm@51507
   310
        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
wenzelm@51507
   311
wenzelm@61865
   312
      val unit = string_width(Symbol.space) max 1.0
wenzelm@51507
   313
      val average = string_width("mix") / (3 * unit)
wenzelm@51507
   314
      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
wenzelm@51492
   315
    }
wenzelm@52873
   316
wenzelm@52873
   317
wenzelm@52873
   318
  /* icons */
wenzelm@52873
   319
wenzelm@52873
   320
  def load_icon(name: String): Icon =
wenzelm@52873
   321
  {
wenzelm@52873
   322
    val name1 =
wenzelm@52873
   323
      if (name.startsWith("idea-icons/")) {
wenzelm@60992
   324
        val file = File.platform_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
wenzelm@52873
   325
        "jar:" + file + "!/" + name
wenzelm@52873
   326
      }
wenzelm@52873
   327
      else name
wenzelm@52873
   328
    val icon = GUIUtilities.loadIcon(name1)
wenzelm@52873
   329
    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
wenzelm@52873
   330
    else icon
wenzelm@52873
   331
  }
wenzelm@52874
   332
wenzelm@52874
   333
  def load_image_icon(name: String): ImageIcon =
wenzelm@52874
   334
    load_icon(name) match {
wenzelm@52874
   335
      case icon: ImageIcon => icon
wenzelm@52874
   336
      case _ => error("Bad image icon: " + name)
wenzelm@52874
   337
    }
wenzelm@53226
   338
wenzelm@53226
   339
wenzelm@53231
   340
  /* key event handling */
wenzelm@53231
   341
wenzelm@56930
   342
  def request_focus_view(alt_view: View = null)
wenzelm@53231
   343
  {
wenzelm@56930
   344
    val view = if (alt_view != null) alt_view else jEdit.getActiveView()
wenzelm@53231
   345
    if (view != null) {
wenzelm@53231
   346
      val text_area = view.getTextArea
wenzelm@53231
   347
      if (text_area != null) text_area.requestFocus
wenzelm@53231
   348
    }
wenzelm@53231
   349
  }
wenzelm@53231
   350
wenzelm@53231
   351
  def propagate_key(view: View, evt: KeyEvent)
wenzelm@53231
   352
  {
wenzelm@53231
   353
    if (view != null && !evt.isConsumed)
wenzelm@53231
   354
      view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
wenzelm@53231
   355
  }
wenzelm@53226
   356
wenzelm@53226
   357
  def key_listener(
wenzelm@53226
   358
    key_typed: KeyEvent => Unit = _ => (),
wenzelm@53226
   359
    key_pressed: KeyEvent => Unit = _ => (),
wenzelm@53226
   360
    key_released: KeyEvent => Unit = _ => ()): KeyListener =
wenzelm@53226
   361
  {
wenzelm@53226
   362
    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
wenzelm@53226
   363
    {
wenzelm@53237
   364
      val evt = KeyEventWorkaround.processKeyEvent(evt0)
wenzelm@53226
   365
      if (evt != null) handle(evt)
wenzelm@53226
   366
    }
wenzelm@53226
   367
wenzelm@53226
   368
    new KeyListener
wenzelm@53226
   369
    {
wenzelm@53226
   370
      def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
wenzelm@53226
   371
      def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
wenzelm@53226
   372
      def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
wenzelm@53226
   373
    }
wenzelm@53226
   374
  }
wenzelm@53784
   375
wenzelm@53784
   376
  def special_key(evt: KeyEvent): Boolean =
wenzelm@53784
   377
  {
wenzelm@59571
   378
    // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
wenzelm@53784
   379
    val mod = evt.getModifiers
wenzelm@53784
   380
    (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
wenzelm@53784
   381
    (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
wenzelm@53784
   382
      !Debug.ALT_KEY_PRESSED_DISABLED ||
wenzelm@53784
   383
    (mod & InputEvent.META_MASK) != 0
wenzelm@53784
   384
  }
wenzelm@49406
   385
}