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