src/Tools/jEdit/src/document_view.scala
author wenzelm
Mon Sep 17 17:56:10 2012 +0200 (2012-09-17)
changeset 49407 215ba6884bdf
parent 49406 38db4832b210
child 49408 3cfc114acd05
permissions -rw-r--r--
tuned signature;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/document_view.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
    Author:     Makarius
wenzelm@36760
     4
wenzelm@36760
     5
Document view connected to jEdit text area.
wenzelm@36760
     6
*/
wenzelm@34408
     7
immler@34403
     8
package isabelle.jedit
immler@34403
     9
wenzelm@34760
    10
wenzelm@36015
    11
import isabelle._
wenzelm@36015
    12
wenzelm@44379
    13
import scala.collection.mutable
wenzelm@45460
    14
import scala.collection.immutable.SortedMap
wenzelm@34784
    15
import scala.actors.Actor._
wenzelm@34784
    16
wenzelm@43520
    17
import java.lang.System
wenzelm@45744
    18
import java.text.BreakIterator
wenzelm@46572
    19
import java.awt.{Color, Graphics2D, Point}
wenzelm@48921
    20
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
wenzelm@39741
    21
  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
wenzelm@34784
    22
import javax.swing.event.{CaretListener, CaretEvent}
wenzelm@34734
    23
wenzelm@43404
    24
import org.gjt.sp.util.Log
wenzelm@43404
    25
wenzelm@42839
    26
import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
wenzelm@34709
    27
import org.gjt.sp.jedit.gui.RolloverButton
wenzelm@39176
    28
import org.gjt.sp.jedit.options.GutterOptionPane
wenzelm@47392
    29
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
wenzelm@43369
    30
import org.gjt.sp.jedit.syntax.{SyntaxStyle}
wenzelm@34784
    31
wenzelm@34784
    32
wenzelm@34784
    33
object Document_View
wenzelm@34784
    34
{
wenzelm@34784
    35
  /* document view of text area */
wenzelm@34784
    36
wenzelm@34784
    37
  private val key = new Object
wenzelm@34784
    38
wenzelm@39741
    39
  def apply(text_area: JEditTextArea): Option[Document_View] =
wenzelm@34784
    40
  {
wenzelm@38223
    41
    Swing_Thread.require()
wenzelm@34784
    42
    text_area.getClientProperty(key) match {
wenzelm@34784
    43
      case doc_view: Document_View => Some(doc_view)
wenzelm@34784
    44
      case _ => None
wenzelm@34784
    45
    }
wenzelm@34784
    46
  }
wenzelm@34784
    47
wenzelm@39741
    48
  def exit(text_area: JEditTextArea)
wenzelm@34784
    49
  {
wenzelm@38223
    50
    Swing_Thread.require()
wenzelm@34788
    51
    apply(text_area) match {
wenzelm@39636
    52
      case None =>
wenzelm@34784
    53
      case Some(doc_view) =>
wenzelm@34784
    54
        doc_view.deactivate()
wenzelm@34784
    55
        text_area.putClientProperty(key, null)
wenzelm@34784
    56
    }
wenzelm@34784
    57
  }
wenzelm@43397
    58
wenzelm@43397
    59
  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
wenzelm@43397
    60
  {
wenzelm@43397
    61
    exit(text_area)
wenzelm@43397
    62
    val doc_view = new Document_View(model, text_area)
wenzelm@43397
    63
    text_area.putClientProperty(key, doc_view)
wenzelm@43397
    64
    doc_view.activate()
wenzelm@43397
    65
    doc_view
wenzelm@43397
    66
  }
wenzelm@34784
    67
}
immler@34403
    68
wenzelm@34733
    69
wenzelm@43376
    70
class Document_View(val model: Document_Model, val text_area: JEditTextArea)
immler@34654
    71
{
wenzelm@34784
    72
  private val session = model.session
wenzelm@34784
    73
immler@34403
    74
wenzelm@43419
    75
  /* robust extension body */
wenzelm@43404
    76
wenzelm@43404
    77
  def robust_body[A](default: A)(body: => A): A =
wenzelm@43417
    78
  {
wenzelm@43417
    79
    try {
wenzelm@43417
    80
      Swing_Thread.require()
wenzelm@43417
    81
      if (model.buffer == text_area.getBuffer) body
wenzelm@43417
    82
      else {
wenzelm@43650
    83
        Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
wenzelm@43417
    84
        default
wenzelm@43404
    85
      }
wenzelm@43404
    86
    }
wenzelm@43417
    87
    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
wenzelm@43417
    88
  }
wenzelm@43404
    89
wenzelm@43404
    90
wenzelm@44378
    91
  /* visible text range */
wenzelm@38881
    92
wenzelm@46815
    93
  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
wenzelm@38881
    94
  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
wenzelm@46812
    95
    Text.Range(start, end min model.buffer.getLength)
wenzelm@38881
    96
wenzelm@46583
    97
  def visible_range(): Option[Text.Range] =
wenzelm@38881
    98
  {
wenzelm@46583
    99
    val n = text_area.getVisibleLines
wenzelm@46583
   100
    if (n > 0) {
wenzelm@46583
   101
      val start = text_area.getScreenLineStartOffset(0)
wenzelm@46583
   102
      val raw_end = text_area.getScreenLineEndOffset(n - 1)
wenzelm@46583
   103
      Some(proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength))
wenzelm@46583
   104
    }
wenzelm@46583
   105
    else None
wenzelm@38881
   106
  }
wenzelm@38881
   107
wenzelm@44378
   108
  def invalidate_range(range: Text.Range)
wenzelm@39132
   109
  {
wenzelm@39132
   110
    text_area.invalidateLineRange(
wenzelm@39132
   111
      model.buffer.getLineOfOffset(range.start),
wenzelm@39132
   112
      model.buffer.getLineOfOffset(range.stop))
wenzelm@39132
   113
  }
wenzelm@39132
   114
wenzelm@38881
   115
wenzelm@44379
   116
  /* perspective */
wenzelm@44379
   117
wenzelm@44379
   118
  def perspective(): Text.Perspective =
wenzelm@44379
   119
  {
wenzelm@44379
   120
    Swing_Thread.require()
wenzelm@44776
   121
    val buffer_range = model.buffer_range()
wenzelm@44473
   122
    Text.Perspective(
wenzelm@44379
   123
      for {
wenzelm@44379
   124
        i <- 0 until text_area.getVisibleLines
wenzelm@46997
   125
        start = text_area.getScreenLineStartOffset(i)
wenzelm@46997
   126
        stop = text_area.getScreenLineEndOffset(i)
wenzelm@44379
   127
        if start >= 0 && stop >= 0
wenzelm@46997
   128
        range <- buffer_range.try_restrict(Text.Range(start, stop))
wenzelm@44583
   129
        if !range.is_singularity
wenzelm@44379
   130
      }
wenzelm@44583
   131
      yield range)
wenzelm@44379
   132
  }
wenzelm@44379
   133
wenzelm@44437
   134
  private def update_perspective = new TextAreaExtension
wenzelm@44437
   135
  {
wenzelm@44437
   136
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@44437
   137
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@44437
   138
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@44437
   139
    {
wenzelm@44437
   140
      model.update_perspective()
wenzelm@44437
   141
    }
wenzelm@44437
   142
  }
wenzelm@44437
   143
wenzelm@44379
   144
wenzelm@49357
   145
  /* active areas within the text */
wenzelm@39740
   146
wenzelm@49357
   147
  private class Active_Area[A](
wenzelm@49357
   148
    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
wenzelm@49357
   149
  {
wenzelm@49357
   150
    private var the_info: Option[Text.Info[A]] = None
wenzelm@34834
   151
wenzelm@49357
   152
    def info: Option[Text.Info[A]] = the_info
wenzelm@38881
   153
wenzelm@49357
   154
    def update(new_info: Option[Text.Info[A]])
wenzelm@49357
   155
    {
wenzelm@49357
   156
      val old_info = the_info
wenzelm@49357
   157
      if (new_info != old_info) {
wenzelm@49357
   158
        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
wenzelm@49357
   159
          invalidate_range(range)
wenzelm@49357
   160
        the_info = new_info
wenzelm@49357
   161
      }
wenzelm@49357
   162
    }
wenzelm@38884
   163
wenzelm@49357
   164
    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
wenzelm@49357
   165
    { update(rendering(r)(range)) }
wenzelm@49357
   166
wenzelm@49357
   167
    def reset { update(None) }
wenzelm@39740
   168
  }
wenzelm@38884
   169
wenzelm@49357
   170
  // owned by Swing thread
wenzelm@48921
   171
wenzelm@40338
   172
  private var control: Boolean = false
wenzelm@40338
   173
wenzelm@49358
   174
  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
wenzelm@49357
   175
  def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
wenzelm@49357
   176
wenzelm@49357
   177
  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
wenzelm@49357
   178
  def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
wenzelm@49357
   179
wenzelm@49357
   180
  private val active_areas = List(highlight_area, hyperlink_area)
wenzelm@49357
   181
  private def active_reset(): Unit = active_areas.foreach(_.reset)
wenzelm@39740
   182
wenzelm@39131
   183
  private val focus_listener = new FocusAdapter {
wenzelm@49357
   184
    override def focusLost(e: FocusEvent) { active_reset() }
wenzelm@39131
   185
  }
wenzelm@39131
   186
wenzelm@39741
   187
  private val window_listener = new WindowAdapter {
wenzelm@49357
   188
    override def windowIconified(e: WindowEvent) { active_reset() }
wenzelm@49357
   189
    override def windowDeactivated(e: WindowEvent) { active_reset() }
wenzelm@39741
   190
  }
wenzelm@39741
   191
wenzelm@48921
   192
  private val mouse_listener = new MouseAdapter {
wenzelm@48921
   193
    override def mouseClicked(e: MouseEvent) {
wenzelm@49357
   194
      hyperlink_area.info match {
wenzelm@48921
   195
        case Some(Text.Info(range, link)) => link.follow(text_area.getView)
wenzelm@48921
   196
        case None =>
wenzelm@48921
   197
      }
wenzelm@48921
   198
    }
wenzelm@48921
   199
  }
wenzelm@48921
   200
wenzelm@39131
   201
  private val mouse_motion_listener = new MouseMotionAdapter {
wenzelm@39131
   202
    override def mouseMoved(e: MouseEvent) {
wenzelm@40338
   203
      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
wenzelm@49357
   204
      if (control && model.buffer.isLoaded) {
wenzelm@49406
   205
        JEdit_Lib.buffer_lock(model.buffer) {
wenzelm@49357
   206
          val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
wenzelm@49407
   207
          val mouse_range =
wenzelm@49407
   208
            JEdit_Lib.point_range(model.buffer, text_area.xyToOffset(e.getX(), e.getY()))
wenzelm@49357
   209
          active_areas.foreach(_.update_rendering(rendering, mouse_range))
wenzelm@39132
   210
        }
wenzelm@49357
   211
      }
wenzelm@49357
   212
      else active_reset()
wenzelm@39131
   213
    }
wenzelm@39131
   214
  }
wenzelm@39131
   215
wenzelm@39131
   216
wenzelm@43381
   217
  /* text area painting */
wenzelm@39044
   218
wenzelm@43381
   219
  private val text_area_painter = new Text_Area_Painter(this)
wenzelm@39700
   220
wenzelm@43381
   221
  private val tooltip_painter = new TextAreaExtension
wenzelm@43381
   222
  {
wenzelm@34784
   223
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   224
    {
wenzelm@43404
   225
      robust_body(null: String) {
wenzelm@49356
   226
        val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
wenzelm@38845
   227
        val offset = text_area.xyToOffset(x, y)
wenzelm@45460
   228
        val range = Text.Range(offset, offset + 1)
wenzelm@46178
   229
        val tip =
wenzelm@49356
   230
          if (control) rendering.tooltip(range)
wenzelm@49356
   231
          else rendering.tooltip_message(range)
wenzelm@46178
   232
        tip.map(Isabelle.tooltip(_)) getOrElse null
wenzelm@34784
   233
      }
wenzelm@34734
   234
    }
immler@34678
   235
  }
immler@34513
   236
wenzelm@42825
   237
  private val gutter_painter = new TextAreaExtension
wenzelm@39175
   238
  {
wenzelm@39175
   239
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@39175
   240
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@39175
   241
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@39175
   242
    {
wenzelm@43404
   243
      robust_body(()) {
wenzelm@46920
   244
        Swing_Thread.assert()
wenzelm@46920
   245
wenzelm@43404
   246
        val gutter = text_area.getGutter
wenzelm@43404
   247
        val width = GutterOptionPane.getSelectionAreaWidth
wenzelm@43404
   248
        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
wenzelm@43404
   249
        val FOLD_MARKER_SIZE = 12
wenzelm@43419
   250
wenzelm@43404
   251
        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
wenzelm@49406
   252
          JEdit_Lib.buffer_lock(model.buffer) {
wenzelm@49356
   253
            val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
wenzelm@49356
   254
wenzelm@43404
   255
            for (i <- 0 until physical_lines.length) {
wenzelm@43404
   256
              if (physical_lines(i) != -1) {
wenzelm@43404
   257
                val line_range = proper_line_range(start(i), end(i))
wenzelm@43419
   258
wenzelm@43404
   259
                // gutter icons
wenzelm@49356
   260
                rendering.gutter_message(line_range) match {
wenzelm@46178
   261
                  case Some(icon) =>
wenzelm@46227
   262
                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
wenzelm@46227
   263
                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
wenzelm@46227
   264
                    icon.paintIcon(gutter, gfx, x0, y0)
wenzelm@46178
   265
                  case None =>
wenzelm@43404
   266
                }
wenzelm@39175
   267
              }
wenzelm@39175
   268
            }
wenzelm@39175
   269
          }
wenzelm@39175
   270
        }
wenzelm@39175
   271
      }
wenzelm@39175
   272
    }
wenzelm@39175
   273
  }
wenzelm@39175
   274
wenzelm@39175
   275
wenzelm@37129
   276
  /* caret handling */
wenzelm@34810
   277
wenzelm@46740
   278
  private val delay_caret_update =
wenzelm@49288
   279
    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
wenzelm@44805
   280
      session.caret_focus.event(Session.Caret_Focus)
wenzelm@34810
   281
    }
wenzelm@46740
   282
wenzelm@46740
   283
  private val caret_listener = new CaretListener {
wenzelm@49195
   284
    override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
wenzelm@34810
   285
  }
wenzelm@34810
   286
wenzelm@34810
   287
wenzelm@46572
   288
  /* text status overview left of scrollbar */
wenzelm@34784
   289
wenzelm@47993
   290
  private object overview extends Text_Overview(this)
wenzelm@46572
   291
  {
wenzelm@46571
   292
    val delay_repaint =
wenzelm@49288
   293
      Swing_Thread.delay_first(
wenzelm@49288
   294
        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
wenzelm@34784
   295
  }
immler@34403
   296
wenzelm@34784
   297
wenzelm@39740
   298
  /* main actor */
wenzelm@39740
   299
wenzelm@39740
   300
  private val main_actor = actor {
wenzelm@39740
   301
    loop {
wenzelm@39740
   302
      react {
wenzelm@49196
   303
        case _: Session.Raw_Edits =>
wenzelm@49196
   304
          Swing_Thread.later {
wenzelm@49288
   305
            overview.delay_repaint.postpone(
wenzelm@49288
   306
              Time.seconds(Isabelle.options.real("editor_input_delay")))
wenzelm@49196
   307
          }
wenzelm@49196
   308
wenzelm@44608
   309
        case changed: Session.Commands_Changed =>
wenzelm@39740
   310
          val buffer = model.buffer
wenzelm@46918
   311
          Swing_Thread.later {
wenzelm@49406
   312
            JEdit_Lib.buffer_lock(buffer) {
wenzelm@46918
   313
              if (model.buffer == text_area.getBuffer) {
wenzelm@47027
   314
                val snapshot = model.snapshot()
wenzelm@39740
   315
wenzelm@47027
   316
                if (changed.assignment ||
wenzelm@46918
   317
                    (changed.nodes.contains(model.name) &&
wenzelm@46918
   318
                     changed.commands.exists(snapshot.node.commands.contains)))
wenzelm@49196
   319
                  Swing_Thread.later { overview.delay_repaint.invoke() }
wenzelm@39740
   320
wenzelm@46918
   321
                visible_range() match {
wenzelm@46918
   322
                  case Some(visible) =>
wenzelm@47027
   323
                    if (changed.assignment) invalidate_range(visible)
wenzelm@46918
   324
                    else {
wenzelm@46918
   325
                      val visible_cmds =
wenzelm@46918
   326
                        snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
wenzelm@46918
   327
                      if (visible_cmds.exists(changed.commands)) {
wenzelm@46918
   328
                        for {
wenzelm@46918
   329
                          line <- 0 until text_area.getVisibleLines
wenzelm@46997
   330
                          start = text_area.getScreenLineStartOffset(line) if start >= 0
wenzelm@46997
   331
                          end = text_area.getScreenLineEndOffset(line) if end >= 0
wenzelm@46997
   332
                          range = proper_line_range(start, end)
wenzelm@46997
   333
                          line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
wenzelm@46918
   334
                          if line_cmds.exists(changed.commands)
wenzelm@46918
   335
                        } text_area.invalidateScreenLineRange(line, line)
wenzelm@46918
   336
                      }
wenzelm@46918
   337
                    }
wenzelm@46918
   338
                  case None =>
wenzelm@46583
   339
                }
wenzelm@46918
   340
              }
wenzelm@39740
   341
            }
wenzelm@39740
   342
          }
wenzelm@39740
   343
wenzelm@39740
   344
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@39740
   345
      }
wenzelm@39740
   346
    }
wenzelm@39740
   347
  }
wenzelm@39740
   348
wenzelm@39740
   349
wenzelm@34784
   350
  /* activation */
wenzelm@34784
   351
wenzelm@34808
   352
  private def activate()
wenzelm@34784
   353
  {
wenzelm@42825
   354
    val painter = text_area.getPainter
wenzelm@44437
   355
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
wenzelm@43387
   356
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
wenzelm@43381
   357
    text_area_painter.activate()
wenzelm@42825
   358
    text_area.getGutter.addExtension(gutter_painter)
wenzelm@39131
   359
    text_area.addFocusListener(focus_listener)
wenzelm@39741
   360
    text_area.getView.addWindowListener(window_listener)
wenzelm@48921
   361
    painter.addMouseListener(mouse_listener)
wenzelm@42825
   362
    painter.addMouseMotionListener(mouse_motion_listener)
wenzelm@34810
   363
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   364
    text_area.addLeftOfScrollBar(overview)
wenzelm@49196
   365
    session.raw_edits += main_actor
wenzelm@39740
   366
    session.commands_changed += main_actor
wenzelm@34784
   367
  }
wenzelm@34784
   368
wenzelm@34808
   369
  private def deactivate()
wenzelm@34784
   370
  {
wenzelm@42825
   371
    val painter = text_area.getPainter
wenzelm@49196
   372
    session.raw_edits -= main_actor
wenzelm@39740
   373
    session.commands_changed -= main_actor
wenzelm@39131
   374
    text_area.removeFocusListener(focus_listener)
wenzelm@39741
   375
    text_area.getView.removeWindowListener(window_listener)
wenzelm@42825
   376
    painter.removeMouseMotionListener(mouse_motion_listener)
wenzelm@48921
   377
    painter.removeMouseListener(mouse_listener)
wenzelm@49195
   378
    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
wenzelm@49195
   379
    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
wenzelm@42825
   380
    text_area.getGutter.removeExtension(gutter_painter)
wenzelm@43381
   381
    text_area_painter.deactivate()
wenzelm@43381
   382
    painter.removeExtension(tooltip_painter)
wenzelm@44437
   383
    painter.removeExtension(update_perspective)
wenzelm@34784
   384
  }
wenzelm@42825
   385
}