src/Tools/jEdit/src/document_view.scala
author wenzelm
Tue Apr 01 23:04:22 2014 +0200 (2014-04-01)
changeset 56356 c3dbaa155ece
parent 56314 9a513737a0b2
child 56373 0605d90be6fc
permissions -rw-r--r--
tuned for-comprehensions -- less structure mapping;
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@34784
    13
import scala.actors.Actor._
wenzelm@34784
    14
wenzelm@54441
    15
import java.awt.Graphics2D
wenzelm@53226
    16
import java.awt.event.KeyEvent
wenzelm@34784
    17
import javax.swing.event.{CaretListener, CaretEvent}
wenzelm@34734
    18
wenzelm@54441
    19
import org.gjt.sp.jedit.jEdit
wenzelm@39176
    20
import org.gjt.sp.jedit.options.GutterOptionPane
wenzelm@55712
    21
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
wenzelm@34784
    22
wenzelm@34784
    23
wenzelm@34784
    24
object Document_View
wenzelm@34784
    25
{
wenzelm@34784
    26
  /* document view of text area */
wenzelm@34784
    27
wenzelm@34784
    28
  private val key = new Object
wenzelm@34784
    29
wenzelm@55712
    30
  def apply(text_area: TextArea): Option[Document_View] =
wenzelm@34784
    31
  {
wenzelm@38223
    32
    Swing_Thread.require()
wenzelm@34784
    33
    text_area.getClientProperty(key) match {
wenzelm@34784
    34
      case doc_view: Document_View => Some(doc_view)
wenzelm@34784
    35
      case _ => None
wenzelm@34784
    36
    }
wenzelm@34784
    37
  }
wenzelm@34784
    38
wenzelm@39741
    39
  def exit(text_area: JEditTextArea)
wenzelm@34784
    40
  {
wenzelm@38223
    41
    Swing_Thread.require()
wenzelm@34788
    42
    apply(text_area) match {
wenzelm@39636
    43
      case None =>
wenzelm@34784
    44
      case Some(doc_view) =>
wenzelm@34784
    45
        doc_view.deactivate()
wenzelm@34784
    46
        text_area.putClientProperty(key, null)
wenzelm@34784
    47
    }
wenzelm@34784
    48
  }
wenzelm@43397
    49
wenzelm@43397
    50
  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
wenzelm@43397
    51
  {
wenzelm@43397
    52
    exit(text_area)
wenzelm@43397
    53
    val doc_view = new Document_View(model, text_area)
wenzelm@43397
    54
    text_area.putClientProperty(key, doc_view)
wenzelm@43397
    55
    doc_view.activate()
wenzelm@43397
    56
    doc_view
wenzelm@43397
    57
  }
wenzelm@34784
    58
}
immler@34403
    59
wenzelm@34733
    60
wenzelm@43376
    61
class Document_View(val model: Document_Model, val text_area: JEditTextArea)
immler@34654
    62
{
wenzelm@34784
    63
  private val session = model.session
wenzelm@34784
    64
wenzelm@50205
    65
  def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
wenzelm@49411
    66
wenzelm@50306
    67
  val rich_text_area =
wenzelm@50915
    68
    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
wenzelm@53179
    69
      caret_visible = true, enable_hovering = false)
wenzelm@49411
    70
immler@34403
    71
wenzelm@44379
    72
  /* perspective */
wenzelm@44379
    73
wenzelm@54325
    74
  def perspective(snapshot: Document.Snapshot): Text.Perspective =
wenzelm@44379
    75
  {
wenzelm@44379
    76
    Swing_Thread.require()
wenzelm@53780
    77
wenzelm@54325
    78
    val active_command =
wenzelm@54325
    79
    {
wenzelm@54325
    80
      val view = text_area.getView
wenzelm@54325
    81
      if (view != null && view.getTextArea == text_area) {
wenzelm@54325
    82
        PIDE.editor.current_command(view, snapshot) match {
wenzelm@54325
    83
          case Some(command) =>
wenzelm@54325
    84
            snapshot.node.command_start(command) match {
wenzelm@54530
    85
              case Some(start) => List(snapshot.convert(command.proper_range + start))
wenzelm@54325
    86
              case None => Nil
wenzelm@54325
    87
            }
wenzelm@54325
    88
          case None => Nil
wenzelm@54325
    89
        }
wenzelm@54325
    90
      }
wenzelm@53780
    91
      else Nil
wenzelm@54325
    92
    }
wenzelm@53780
    93
wenzelm@50363
    94
    val buffer_range = JEdit_Lib.buffer_range(model.buffer)
wenzelm@53780
    95
    val visible_lines =
wenzelm@53780
    96
      (for {
wenzelm@56356
    97
        i <- (0 until text_area.getVisibleLines).iterator
wenzelm@46997
    98
        start = text_area.getScreenLineStartOffset(i)
wenzelm@46997
    99
        stop = text_area.getScreenLineEndOffset(i)
wenzelm@44379
   100
        if start >= 0 && stop >= 0
wenzelm@46997
   101
        range <- buffer_range.try_restrict(Text.Range(start, stop))
wenzelm@44583
   102
        if !range.is_singularity
wenzelm@44379
   103
      }
wenzelm@53780
   104
      yield range).toList
wenzelm@53780
   105
wenzelm@54325
   106
    Text.Perspective(active_command ::: visible_lines)
wenzelm@44379
   107
  }
wenzelm@44379
   108
wenzelm@54461
   109
  private def update_view = 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@49424
   115
      // no robust_body
wenzelm@54461
   116
      PIDE.editor.invoke()
wenzelm@44437
   117
    }
wenzelm@44437
   118
  }
wenzelm@44437
   119
wenzelm@44379
   120
wenzelm@49411
   121
  /* gutter */
immler@34513
   122
wenzelm@42825
   123
  private val gutter_painter = new TextAreaExtension
wenzelm@39175
   124
  {
wenzelm@39175
   125
    override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@39175
   126
      first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@39175
   127
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@39175
   128
    {
wenzelm@49411
   129
      rich_text_area.robust_body(()) {
wenzelm@46920
   130
        Swing_Thread.assert()
wenzelm@46920
   131
wenzelm@43404
   132
        val gutter = text_area.getGutter
wenzelm@43404
   133
        val width = GutterOptionPane.getSelectionAreaWidth
wenzelm@43404
   134
        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
wenzelm@43404
   135
        val FOLD_MARKER_SIZE = 12
wenzelm@43419
   136
wenzelm@43404
   137
        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
wenzelm@49408
   138
          val buffer = model.buffer
wenzelm@49408
   139
          JEdit_Lib.buffer_lock(buffer) {
wenzelm@49410
   140
            val rendering = get_rendering()
wenzelm@49356
   141
wenzelm@43404
   142
            for (i <- 0 until physical_lines.length) {
wenzelm@43404
   143
              if (physical_lines(i) != -1) {
wenzelm@49843
   144
                val line_range = Text.Range(start(i), end(i))
wenzelm@43419
   145
wenzelm@43404
   146
                // gutter icons
wenzelm@49356
   147
                rendering.gutter_message(line_range) match {
wenzelm@46178
   148
                  case Some(icon) =>
wenzelm@46227
   149
                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
wenzelm@46227
   150
                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
wenzelm@46227
   151
                    icon.paintIcon(gutter, gfx, x0, y0)
wenzelm@46178
   152
                  case None =>
wenzelm@43404
   153
                }
wenzelm@39175
   154
              }
wenzelm@39175
   155
            }
wenzelm@39175
   156
          }
wenzelm@39175
   157
        }
wenzelm@39175
   158
      }
wenzelm@39175
   159
    }
wenzelm@39175
   160
  }
wenzelm@39175
   161
wenzelm@39175
   162
wenzelm@52479
   163
  /* key listener */
wenzelm@52479
   164
wenzelm@53226
   165
  private val key_listener =
wenzelm@53226
   166
    JEdit_Lib.key_listener(
wenzelm@53227
   167
      key_pressed = (evt: KeyEvent) =>
wenzelm@53226
   168
        {
wenzelm@53244
   169
          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
wenzelm@53226
   170
            evt.consume
wenzelm@53274
   171
        }
wenzelm@53226
   172
    )
wenzelm@52479
   173
wenzelm@52479
   174
wenzelm@37129
   175
  /* caret handling */
wenzelm@34810
   176
wenzelm@46740
   177
  private val delay_caret_update =
wenzelm@50207
   178
    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
wenzelm@44805
   179
      session.caret_focus.event(Session.Caret_Focus)
wenzelm@34810
   180
    }
wenzelm@46740
   181
wenzelm@46740
   182
  private val caret_listener = new CaretListener {
wenzelm@49195
   183
    override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
wenzelm@34810
   184
  }
wenzelm@34810
   185
wenzelm@34810
   186
wenzelm@46572
   187
  /* text status overview left of scrollbar */
wenzelm@34784
   188
wenzelm@47993
   189
  private object overview extends Text_Overview(this)
wenzelm@46572
   190
  {
wenzelm@46571
   191
    val delay_repaint =
wenzelm@50207
   192
      Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
wenzelm@34784
   193
  }
immler@34403
   194
wenzelm@34784
   195
wenzelm@39740
   196
  /* main actor */
wenzelm@39740
   197
wenzelm@39740
   198
  private val main_actor = actor {
wenzelm@39740
   199
    loop {
wenzelm@39740
   200
      react {
wenzelm@49196
   201
        case _: Session.Raw_Edits =>
wenzelm@49196
   202
          Swing_Thread.later {
wenzelm@50207
   203
            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
wenzelm@49196
   204
          }
wenzelm@49196
   205
wenzelm@44608
   206
        case changed: Session.Commands_Changed =>
wenzelm@39740
   207
          val buffer = model.buffer
wenzelm@46918
   208
          Swing_Thread.later {
wenzelm@49406
   209
            JEdit_Lib.buffer_lock(buffer) {
wenzelm@46918
   210
              if (model.buffer == text_area.getBuffer) {
wenzelm@47027
   211
                val snapshot = model.snapshot()
wenzelm@39740
   212
wenzelm@56314
   213
                val load_changed =
wenzelm@56314
   214
                  snapshot.load_commands.exists(changed.commands.contains)
wenzelm@55432
   215
wenzelm@56314
   216
                if (changed.assignment || load_changed ||
wenzelm@52973
   217
                    (changed.nodes.contains(model.node_name) &&
wenzelm@46918
   218
                     changed.commands.exists(snapshot.node.commands.contains)))
wenzelm@49196
   219
                  Swing_Thread.later { overview.delay_repaint.invoke() }
wenzelm@39740
   220
wenzelm@50770
   221
                val visible_lines = text_area.getVisibleLines
wenzelm@50770
   222
                if (visible_lines > 0) {
wenzelm@56314
   223
                  if (changed.assignment || load_changed)
wenzelm@55432
   224
                    text_area.invalidateScreenLineRange(0, visible_lines)
wenzelm@50770
   225
                  else {
wenzelm@50770
   226
                    val visible_range = JEdit_Lib.visible_range(text_area).get
wenzelm@50770
   227
                    val visible_cmds =
wenzelm@50770
   228
                      snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
wenzelm@50770
   229
                    if (visible_cmds.exists(changed.commands)) {
wenzelm@50770
   230
                      for {
wenzelm@56356
   231
                        line <- (0 until visible_lines).iterator
wenzelm@50770
   232
                        start = text_area.getScreenLineStartOffset(line) if start >= 0
wenzelm@50770
   233
                        end = text_area.getScreenLineEndOffset(line) if end >= 0
wenzelm@50770
   234
                        range = Text.Range(start, end)
wenzelm@50770
   235
                        line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
wenzelm@50770
   236
                        if line_cmds.exists(changed.commands)
wenzelm@50770
   237
                      } text_area.invalidateScreenLineRange(line, line)
wenzelm@46918
   238
                    }
wenzelm@50770
   239
                  }
wenzelm@46583
   240
                }
wenzelm@46918
   241
              }
wenzelm@39740
   242
            }
wenzelm@39740
   243
          }
wenzelm@39740
   244
wenzelm@54441
   245
        case bad =>
wenzelm@55618
   246
          System.err.println("command_change_actor: ignoring bad message " + bad)
wenzelm@39740
   247
      }
wenzelm@39740
   248
    }
wenzelm@39740
   249
  }
wenzelm@39740
   250
wenzelm@39740
   251
wenzelm@34784
   252
  /* activation */
wenzelm@34784
   253
wenzelm@34808
   254
  private def activate()
wenzelm@34784
   255
  {
wenzelm@42825
   256
    val painter = text_area.getPainter
wenzelm@49410
   257
wenzelm@54461
   258
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_view)
wenzelm@49411
   259
    rich_text_area.activate()
wenzelm@42825
   260
    text_area.getGutter.addExtension(gutter_painter)
wenzelm@52479
   261
    text_area.addKeyListener(key_listener)
wenzelm@34810
   262
    text_area.addCaretListener(caret_listener)
wenzelm@34810
   263
    text_area.addLeftOfScrollBar(overview)
wenzelm@49196
   264
    session.raw_edits += main_actor
wenzelm@39740
   265
    session.commands_changed += main_actor
wenzelm@34784
   266
  }
wenzelm@34784
   267
wenzelm@34808
   268
  private def deactivate()
wenzelm@34784
   269
  {
wenzelm@42825
   270
    val painter = text_area.getPainter
wenzelm@49410
   271
wenzelm@49196
   272
    session.raw_edits -= main_actor
wenzelm@39740
   273
    session.commands_changed -= main_actor
wenzelm@52479
   274
    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
wenzelm@49195
   275
    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
wenzelm@52479
   276
    text_area.removeKeyListener(key_listener)
wenzelm@42825
   277
    text_area.getGutter.removeExtension(gutter_painter)
wenzelm@49411
   278
    rich_text_area.deactivate()
wenzelm@54461
   279
    painter.removeExtension(update_view)
wenzelm@34784
   280
  }
wenzelm@42825
   281
}