src/Tools/jEdit/src/document_view.scala
author wenzelm
Mon Sep 17 18:06:34 2012 +0200 (2012-09-17)
changeset 49408 3cfc114acd05
parent 49407 215ba6884bdf
child 49410 34acbcc33adf
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@44379
    91
  /* perspective */
wenzelm@44379
    92
wenzelm@44379
    93
  def perspective(): Text.Perspective =
wenzelm@44379
    94
  {
wenzelm@44379
    95
    Swing_Thread.require()
wenzelm@44776
    96
    val buffer_range = model.buffer_range()
wenzelm@44473
    97
    Text.Perspective(
wenzelm@44379
    98
      for {
wenzelm@44379
    99
        i <- 0 until text_area.getVisibleLines
wenzelm@46997
   100
        start = text_area.getScreenLineStartOffset(i)
wenzelm@46997
   101
        stop = text_area.getScreenLineEndOffset(i)
wenzelm@44379
   102
        if start >= 0 && stop >= 0
wenzelm@46997
   103
        range <- buffer_range.try_restrict(Text.Range(start, stop))
wenzelm@44583
   104
        if !range.is_singularity
wenzelm@44379
   105
      }
wenzelm@44583
   106
      yield range)
wenzelm@44379
   107
  }
wenzelm@44379
   108
wenzelm@44437
   109
  private def update_perspective = new TextAreaExtension
wenzelm@44437
   110
  {
wenzelm@44437
   111
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@44437
   112
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@44437
   113
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@44437
   114
    {
wenzelm@44437
   115
      model.update_perspective()
wenzelm@44437
   116
    }
wenzelm@44437
   117
  }
wenzelm@44437
   118
wenzelm@44379
   119
wenzelm@49357
   120
  /* active areas within the text */
wenzelm@39740
   121
wenzelm@49357
   122
  private class Active_Area[A](
wenzelm@49357
   123
    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
wenzelm@49357
   124
  {
wenzelm@49357
   125
    private var the_info: Option[Text.Info[A]] = None
wenzelm@34834
   126
wenzelm@49357
   127
    def info: Option[Text.Info[A]] = the_info
wenzelm@38881
   128
wenzelm@49357
   129
    def update(new_info: Option[Text.Info[A]])
wenzelm@49357
   130
    {
wenzelm@49357
   131
      val old_info = the_info
wenzelm@49357
   132
      if (new_info != old_info) {
wenzelm@49357
   133
        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
wenzelm@49408
   134
          JEdit_Lib.invalidate_range(text_area, range)
wenzelm@49357
   135
        the_info = new_info
wenzelm@49357
   136
      }
wenzelm@49357
   137
    }
wenzelm@38884
   138
wenzelm@49357
   139
    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
wenzelm@49357
   140
    { update(rendering(r)(range)) }
wenzelm@49357
   141
wenzelm@49357
   142
    def reset { update(None) }
wenzelm@39740
   143
  }
wenzelm@38884
   144
wenzelm@49357
   145
  // owned by Swing thread
wenzelm@48921
   146
wenzelm@40338
   147
  private var control: Boolean = false
wenzelm@40338
   148
wenzelm@49358
   149
  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
wenzelm@49357
   150
  def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
wenzelm@49357
   151
wenzelm@49357
   152
  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
wenzelm@49357
   153
  def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
wenzelm@49357
   154
wenzelm@49357
   155
  private val active_areas = List(highlight_area, hyperlink_area)
wenzelm@49357
   156
  private def active_reset(): Unit = active_areas.foreach(_.reset)
wenzelm@39740
   157
wenzelm@39131
   158
  private val focus_listener = new FocusAdapter {
wenzelm@49357
   159
    override def focusLost(e: FocusEvent) { active_reset() }
wenzelm@39131
   160
  }
wenzelm@39131
   161
wenzelm@39741
   162
  private val window_listener = new WindowAdapter {
wenzelm@49357
   163
    override def windowIconified(e: WindowEvent) { active_reset() }
wenzelm@49357
   164
    override def windowDeactivated(e: WindowEvent) { active_reset() }
wenzelm@39741
   165
  }
wenzelm@39741
   166
wenzelm@48921
   167
  private val mouse_listener = new MouseAdapter {
wenzelm@48921
   168
    override def mouseClicked(e: MouseEvent) {
wenzelm@49357
   169
      hyperlink_area.info match {
wenzelm@48921
   170
        case Some(Text.Info(range, link)) => link.follow(text_area.getView)
wenzelm@48921
   171
        case None =>
wenzelm@48921
   172
      }
wenzelm@48921
   173
    }
wenzelm@48921
   174
  }
wenzelm@48921
   175
wenzelm@39131
   176
  private val mouse_motion_listener = new MouseMotionAdapter {
wenzelm@39131
   177
    override def mouseMoved(e: MouseEvent) {
wenzelm@40338
   178
      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
wenzelm@49357
   179
      if (control && model.buffer.isLoaded) {
wenzelm@49406
   180
        JEdit_Lib.buffer_lock(model.buffer) {
wenzelm@49357
   181
          val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
wenzelm@49407
   182
          val mouse_range =
wenzelm@49407
   183
            JEdit_Lib.point_range(model.buffer, text_area.xyToOffset(e.getX(), e.getY()))
wenzelm@49357
   184
          active_areas.foreach(_.update_rendering(rendering, mouse_range))
wenzelm@39132
   185
        }
wenzelm@49357
   186
      }
wenzelm@49357
   187
      else active_reset()
wenzelm@39131
   188
    }
wenzelm@39131
   189
  }
wenzelm@39131
   190
wenzelm@39131
   191
wenzelm@43381
   192
  /* text area painting */
wenzelm@39044
   193
wenzelm@43381
   194
  private val text_area_painter = new Text_Area_Painter(this)
wenzelm@39700
   195
wenzelm@43381
   196
  private val tooltip_painter = new TextAreaExtension
wenzelm@43381
   197
  {
wenzelm@34784
   198
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34784
   199
    {
wenzelm@43404
   200
      robust_body(null: String) {
wenzelm@49356
   201
        val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
wenzelm@38845
   202
        val offset = text_area.xyToOffset(x, y)
wenzelm@45460
   203
        val range = Text.Range(offset, offset + 1)
wenzelm@46178
   204
        val tip =
wenzelm@49356
   205
          if (control) rendering.tooltip(range)
wenzelm@49356
   206
          else rendering.tooltip_message(range)
wenzelm@46178
   207
        tip.map(Isabelle.tooltip(_)) getOrElse null
wenzelm@34784
   208
      }
wenzelm@34734
   209
    }
immler@34678
   210
  }
immler@34513
   211
wenzelm@42825
   212
  private val gutter_painter = new TextAreaExtension
wenzelm@39175
   213
  {
wenzelm@39175
   214
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@39175
   215
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@39175
   216
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@39175
   217
    {
wenzelm@43404
   218
      robust_body(()) {
wenzelm@46920
   219
        Swing_Thread.assert()
wenzelm@46920
   220
wenzelm@43404
   221
        val gutter = text_area.getGutter
wenzelm@43404
   222
        val width = GutterOptionPane.getSelectionAreaWidth
wenzelm@43404
   223
        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
wenzelm@43404
   224
        val FOLD_MARKER_SIZE = 12
wenzelm@43419
   225
wenzelm@43404
   226
        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
wenzelm@49408
   227
          val buffer = model.buffer
wenzelm@49408
   228
          JEdit_Lib.buffer_lock(buffer) {
wenzelm@49356
   229
            val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
wenzelm@49356
   230
wenzelm@43404
   231
            for (i <- 0 until physical_lines.length) {
wenzelm@43404
   232
              if (physical_lines(i) != -1) {
wenzelm@49408
   233
                val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
wenzelm@43419
   234
wenzelm@43404
   235
                // gutter icons
wenzelm@49356
   236
                rendering.gutter_message(line_range) match {
wenzelm@46178
   237
                  case Some(icon) =>
wenzelm@46227
   238
                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
wenzelm@46227
   239
                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
wenzelm@46227
   240
                    icon.paintIcon(gutter, gfx, x0, y0)
wenzelm@46178
   241
                  case None =>
wenzelm@43404
   242
                }
wenzelm@39175
   243
              }
wenzelm@39175
   244
            }
wenzelm@39175
   245
          }
wenzelm@39175
   246
        }
wenzelm@39175
   247
      }
wenzelm@39175
   248
    }
wenzelm@39175
   249
  }
wenzelm@39175
   250
wenzelm@39175
   251
wenzelm@37129
   252
  /* caret handling */
wenzelm@34810
   253
wenzelm@46740
   254
  private val delay_caret_update =
wenzelm@49288
   255
    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
wenzelm@44805
   256
      session.caret_focus.event(Session.Caret_Focus)
wenzelm@34810
   257
    }
wenzelm@46740
   258
wenzelm@46740
   259
  private val caret_listener = new CaretListener {
wenzelm@49195
   260
    override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
wenzelm@34810
   261
  }
wenzelm@34810
   262
wenzelm@34810
   263
wenzelm@46572
   264
  /* text status overview left of scrollbar */
wenzelm@34784
   265
wenzelm@47993
   266
  private object overview extends Text_Overview(this)
wenzelm@46572
   267
  {
wenzelm@46571
   268
    val delay_repaint =
wenzelm@49288
   269
      Swing_Thread.delay_first(
wenzelm@49288
   270
        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
wenzelm@34784
   271
  }
immler@34403
   272
wenzelm@34784
   273
wenzelm@39740
   274
  /* main actor */
wenzelm@39740
   275
wenzelm@39740
   276
  private val main_actor = actor {
wenzelm@39740
   277
    loop {
wenzelm@39740
   278
      react {
wenzelm@49196
   279
        case _: Session.Raw_Edits =>
wenzelm@49196
   280
          Swing_Thread.later {
wenzelm@49288
   281
            overview.delay_repaint.postpone(
wenzelm@49288
   282
              Time.seconds(Isabelle.options.real("editor_input_delay")))
wenzelm@49196
   283
          }
wenzelm@49196
   284
wenzelm@44608
   285
        case changed: Session.Commands_Changed =>
wenzelm@39740
   286
          val buffer = model.buffer
wenzelm@46918
   287
          Swing_Thread.later {
wenzelm@49406
   288
            JEdit_Lib.buffer_lock(buffer) {
wenzelm@46918
   289
              if (model.buffer == text_area.getBuffer) {
wenzelm@47027
   290
                val snapshot = model.snapshot()
wenzelm@39740
   291
wenzelm@47027
   292
                if (changed.assignment ||
wenzelm@46918
   293
                    (changed.nodes.contains(model.name) &&
wenzelm@46918
   294
                     changed.commands.exists(snapshot.node.commands.contains)))
wenzelm@49196
   295
                  Swing_Thread.later { overview.delay_repaint.invoke() }
wenzelm@39740
   296
wenzelm@49408
   297
                JEdit_Lib.visible_range(text_area) match {
wenzelm@46918
   298
                  case Some(visible) =>
wenzelm@49408
   299
                    if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible)
wenzelm@46918
   300
                    else {
wenzelm@46918
   301
                      val visible_cmds =
wenzelm@46918
   302
                        snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
wenzelm@46918
   303
                      if (visible_cmds.exists(changed.commands)) {
wenzelm@46918
   304
                        for {
wenzelm@46918
   305
                          line <- 0 until text_area.getVisibleLines
wenzelm@46997
   306
                          start = text_area.getScreenLineStartOffset(line) if start >= 0
wenzelm@46997
   307
                          end = text_area.getScreenLineEndOffset(line) if end >= 0
wenzelm@49408
   308
                          range = JEdit_Lib.proper_line_range(buffer, start, end)
wenzelm@46997
   309
                          line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
wenzelm@46918
   310
                          if line_cmds.exists(changed.commands)
wenzelm@46918
   311
                        } text_area.invalidateScreenLineRange(line, line)
wenzelm@46918
   312
                      }
wenzelm@46918
   313
                    }
wenzelm@46918
   314
                  case None =>
wenzelm@46583
   315
                }
wenzelm@46918
   316
              }
wenzelm@39740
   317
            }
wenzelm@39740
   318
          }
wenzelm@39740
   319
wenzelm@39740
   320
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@39740
   321
      }
wenzelm@39740
   322
    }
wenzelm@39740
   323
  }
wenzelm@39740
   324
wenzelm@39740
   325
wenzelm@34784
   326
  /* activation */
wenzelm@34784
   327
wenzelm@34808
   328
  private def activate()
wenzelm@34784
   329
  {
wenzelm@42825
   330
    val painter = text_area.getPainter
wenzelm@44437
   331
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
wenzelm@43387
   332
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
wenzelm@43381
   333
    text_area_painter.activate()
wenzelm@42825
   334
    text_area.getGutter.addExtension(gutter_painter)
wenzelm@39131
   335
    text_area.addFocusListener(focus_listener)
wenzelm@39741
   336
    text_area.getView.addWindowListener(window_listener)
wenzelm@48921
   337
    painter.addMouseListener(mouse_listener)
wenzelm@42825
   338
    painter.addMouseMotionListener(mouse_motion_listener)
wenzelm@34810
   339
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   340
    text_area.addLeftOfScrollBar(overview)
wenzelm@49196
   341
    session.raw_edits += main_actor
wenzelm@39740
   342
    session.commands_changed += main_actor
wenzelm@34784
   343
  }
wenzelm@34784
   344
wenzelm@34808
   345
  private def deactivate()
wenzelm@34784
   346
  {
wenzelm@42825
   347
    val painter = text_area.getPainter
wenzelm@49196
   348
    session.raw_edits -= main_actor
wenzelm@39740
   349
    session.commands_changed -= main_actor
wenzelm@39131
   350
    text_area.removeFocusListener(focus_listener)
wenzelm@39741
   351
    text_area.getView.removeWindowListener(window_listener)
wenzelm@42825
   352
    painter.removeMouseMotionListener(mouse_motion_listener)
wenzelm@48921
   353
    painter.removeMouseListener(mouse_listener)
wenzelm@49195
   354
    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
wenzelm@49195
   355
    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
wenzelm@42825
   356
    text_area.getGutter.removeExtension(gutter_painter)
wenzelm@43381
   357
    text_area_painter.deactivate()
wenzelm@43381
   358
    painter.removeExtension(tooltip_painter)
wenzelm@44437
   359
    painter.removeExtension(update_perspective)
wenzelm@34784
   360
  }
wenzelm@42825
   361
}