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