src/Tools/jEdit/src/jedit/TheoryView.scala
author wenzelm
Tue Jun 02 22:31:58 2009 +0200 (2009-06-02)
changeset 34588 e8ac8794971f
parent 34583 17c83413b7fe
child 34598 4f2d122c0a67
permissions -rw-r--r--
superficial tuning;
wenzelm@34407
     1
/*
wenzelm@34408
     2
 * jEdit text area as document text source
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Fabian Immler, TU Munich
wenzelm@34407
     5
 * @author Johannes Hölzl, TU Munich
wenzelm@34447
     6
 * @author Makarius
wenzelm@34407
     7
 */
wenzelm@34407
     8
wenzelm@34318
     9
package isabelle.jedit
wenzelm@34318
    10
immler@34532
    11
import scala.actors.Actor
wenzelm@34582
    12
import scala.actors.Actor._
wenzelm@34446
    13
wenzelm@34318
    14
import isabelle.proofdocument.Text
wenzelm@34452
    15
import isabelle.prover.{Prover, Command}
wenzelm@34318
    16
wenzelm@34318
    17
import java.awt.Graphics2D
wenzelm@34446
    18
import java.awt.event.{ActionEvent, ActionListener}
wenzelm@34446
    19
import java.awt.Color
wenzelm@34447
    20
import javax.swing.Timer
wenzelm@34447
    21
import javax.swing.event.{CaretListener, CaretEvent}
wenzelm@34318
    22
wenzelm@34446
    23
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
wenzelm@34446
    24
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
wenzelm@34318
    25
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@34318
    26
wenzelm@34446
    27
wenzelm@34588
    28
object TheoryView
wenzelm@34588
    29
{
wenzelm@34318
    30
immler@34574
    31
  val MAX_CHANGE_LENGTH = 1500
immler@34574
    32
  
wenzelm@34446
    33
  def choose_color(state: Command): Color = {
wenzelm@34448
    34
    if (state == null) Color.red
wenzelm@34318
    35
    else
wenzelm@34458
    36
      state.status match {
wenzelm@34458
    37
        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
wenzelm@34458
    38
        case Command.Status.FINISHED => new Color(234, 248, 255)
wenzelm@34458
    39
        case Command.Status.FAILED => new Color(255, 192, 192)
wenzelm@34318
    40
        case _ => Color.red
wenzelm@34318
    41
      }
wenzelm@34318
    42
  }
wenzelm@34318
    43
}
wenzelm@34318
    44
wenzelm@34446
    45
immler@34532
    46
class TheoryView (text_area: JEditTextArea, document_actor: Actor)
wenzelm@34588
    47
    extends TextAreaExtension with BufferListener
wenzelm@34588
    48
{
immler@34406
    49
wenzelm@34582
    50
  def id() = Isabelle.plugin.id()
immler@34541
    51
  
wenzelm@34446
    52
  private val buffer = text_area.getBuffer
immler@34475
    53
  private val prover = Isabelle.prover_setup(buffer).get.prover
immler@34406
    54
  buffer.addBufferListener(this)
wenzelm@34446
    55
wenzelm@34446
    56
immler@34526
    57
  private var col: Text.Change = null
wenzelm@34446
    58
wenzelm@34446
    59
  private val col_timer = new Timer(300, new ActionListener() {
immler@34515
    60
    override def actionPerformed(e: ActionEvent) = commit
wenzelm@34318
    61
  })
immler@34406
    62
wenzelm@34446
    63
  col_timer.stop
wenzelm@34446
    64
  col_timer.setRepeats(true)
wenzelm@34446
    65
wenzelm@34446
    66
immler@34566
    67
  private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current)
wenzelm@34446
    68
wenzelm@34318
    69
wenzelm@34446
    70
  /* activation */
wenzelm@34446
    71
wenzelm@34446
    72
  private val selected_state_controller = new CaretListener {
wenzelm@34446
    73
    override def caretUpdate(e: CaretEvent) = {
immler@34554
    74
      val doc = prover.document
immler@34554
    75
      val cmd = doc.find_command_at(e.getDot)
immler@34554
    76
      if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
immler@34475
    77
          Isabelle.prover_setup(buffer).get.selected_state != cmd)
immler@34475
    78
        Isabelle.prover_setup(buffer).get.selected_state = cmd
wenzelm@34318
    79
    }
wenzelm@34318
    80
  }
wenzelm@34318
    81
wenzelm@34582
    82
  def activate() {
wenzelm@34446
    83
    text_area.addCaretListener(selected_state_controller)
wenzelm@34446
    84
    text_area.addLeftOfScrollBar(phase_overview)
wenzelm@34446
    85
    text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
immler@34538
    86
    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
wenzelm@34446
    87
  }
wenzelm@34446
    88
wenzelm@34582
    89
  def deactivate() {
wenzelm@34446
    90
    text_area.getPainter.removeExtension(this)
wenzelm@34446
    91
    text_area.removeLeftOfScrollBar(phase_overview)
wenzelm@34446
    92
    text_area.removeCaretListener(selected_state_controller)
wenzelm@34446
    93
  }
wenzelm@34446
    94
wenzelm@34446
    95
wenzelm@34446
    96
  /* painting */
wenzelm@34446
    97
wenzelm@34446
    98
  val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
immler@34538
    99
  
wenzelm@34582
   100
  val change_receiver = actor {
wenzelm@34582
   101
    loop {
wenzelm@34582
   102
      react {
wenzelm@34582
   103
        case _ => {       // FIXME potentially blocking within loop/react!?!?!?!
immler@34541
   104
          Swing.now {
immler@34538
   105
            repaint_delay.delay_or_ignore()
immler@34538
   106
            phase_overview.repaint_delay.delay_or_ignore()
immler@34541
   107
          }
immler@34538
   108
        }
immler@34538
   109
      }
immler@34538
   110
    }
wenzelm@34583
   111
  }
wenzelm@34446
   112
immler@34545
   113
  def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int =
immler@34545
   114
    changes match {
immler@34545
   115
      case Nil => pos
immler@34545
   116
      case Text.Change(id, start, added, removed) :: rest_changes => {
wenzelm@34582
   117
        val shifted =
wenzelm@34582
   118
          if (start <= pos)
immler@34545
   119
            if (pos < start + added.length) start
immler@34545
   120
            else pos - added.length + removed
immler@34545
   121
          else pos
immler@34547
   122
        if (id == to_id) pos
immler@34545
   123
        else _from_current(to_id, rest_changes, shifted)
immler@34545
   124
      }
immler@34545
   125
    }
wenzelm@34446
   126
immler@34545
   127
  def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int =
immler@34545
   128
    changes match {
immler@34545
   129
      case Nil => pos
immler@34545
   130
      case Text.Change(id, start, added, removed) :: rest_changes => {
immler@34547
   131
        val shifted = _to_current(from_id, rest_changes, pos)
immler@34547
   132
        if (id == from_id) pos
immler@34547
   133
        else if (start <= shifted) {
immler@34545
   134
          if (shifted < start + removed) start
immler@34545
   135
          else shifted + added.length - removed
immler@34547
   136
        } else shifted
immler@34545
   137
      }
immler@34545
   138
    }
immler@34545
   139
wenzelm@34588
   140
  def to_current(from_id: String, pos: Int) =
immler@34546
   141
    _to_current(from_id, if (col == null) changes else col :: changes, pos)
wenzelm@34588
   142
  def from_current(to_id: String, pos: Int) =
immler@34546
   143
    _from_current(to_id, if (col == null) changes else col :: changes, pos)
immler@34568
   144
  def to_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
immler@34568
   145
    to_current(document.id, pos)
immler@34568
   146
  def from_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
immler@34568
   147
    from_current(document.id, pos)
wenzelm@34446
   148
wenzelm@34446
   149
  def repaint(cmd: Command) =
wenzelm@34318
   150
  {
immler@34545
   151
    val document = prover.document
wenzelm@34507
   152
    if (text_area != null) {
immler@34554
   153
      val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document)))
immler@34554
   154
      val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1)
immler@34406
   155
      text_area.invalidateLineRange(start, stop)
wenzelm@34446
   156
immler@34475
   157
      if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
immler@34475
   158
        Isabelle.prover_setup(buffer).get.selected_state = cmd  // update State view
wenzelm@34318
   159
    }
wenzelm@34318
   160
  }
wenzelm@34446
   161
wenzelm@34588
   162
  def repaint_all()
wenzelm@34318
   163
  {
immler@34406
   164
    if (text_area != null)
wenzelm@34446
   165
      text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
wenzelm@34318
   166
  }
immler@34391
   167
wenzelm@34446
   168
  def encolor(gfx: Graphics2D,
wenzelm@34588
   169
    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
wenzelm@34446
   170
  {
wenzelm@34446
   171
    val start = text_area.offsetToXY(begin)
wenzelm@34446
   172
    val stop =
wenzelm@34446
   173
      if (finish < buffer.getLength) text_area.offsetToXY(finish)
wenzelm@34446
   174
      else {
wenzelm@34446
   175
        val p = text_area.offsetToXY(finish - 1)
immler@34515
   176
        val metrics = text_area.getPainter.getFontMetrics
immler@34515
   177
        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
wenzelm@34446
   178
        p
immler@34391
   179
      }
wenzelm@34446
   180
wenzelm@34446
   181
    if (start != null && stop != null) {
wenzelm@34446
   182
      gfx.setColor(color)
wenzelm@34446
   183
      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
wenzelm@34446
   184
      else gfx.drawRect(start.x, y, stop.x - start.x, height)
wenzelm@34446
   185
    }
immler@34391
   186
  }
immler@34391
   187
wenzelm@34446
   188
wenzelm@34446
   189
  /* TextAreaExtension methods */
wenzelm@34446
   190
wenzelm@34446
   191
  override def paintValidLine(gfx: Graphics2D,
wenzelm@34588
   192
    screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@34446
   193
  {
immler@34545
   194
    val document = prover.document
immler@34545
   195
    def from_current(pos: Int) = this.from_current(document.id, pos)
immler@34545
   196
    def to_current(pos: Int) = this.to_current(document.id, pos)
wenzelm@34446
   197
    val saved_color = gfx.getColor
wenzelm@34446
   198
wenzelm@34446
   199
    val metrics = text_area.getPainter.getFontMetrics
immler@34545
   200
    var e = document.find_command_at(from_current(start))
immler@34554
   201
    val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)).
immler@34554
   202
      takeWhile(c => to_current(c.start(document)) < end)
wenzelm@34446
   203
    // encolor phase
immler@34526
   204
    for (e <- commands) {
immler@34554
   205
      val begin = start max to_current(e.start(document))
immler@34554
   206
      val finish = end - 1 min to_current(e.stop(document))
wenzelm@34446
   207
      encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
wenzelm@34318
   208
    }
immler@34391
   209
wenzelm@34446
   210
    gfx.setColor(saved_color)
wenzelm@34318
   211
  }
wenzelm@34446
   212
immler@34562
   213
  override def getToolTipText(x: Int, y: Int) = {
immler@34562
   214
    val document = prover.document
immler@34562
   215
    val offset = from_current(document.id, text_area.xyToOffset(x, y))
immler@34562
   216
    val cmd = document.find_command_at(offset)
immler@34562
   217
    if (cmd != null) {
immler@34562
   218
      document.token_start(cmd.tokens.first)
immler@34562
   219
      cmd.type_at(offset - cmd.start(document))
immler@34562
   220
    } else null
immler@34562
   221
  }
immler@34562
   222
wenzelm@34446
   223
  /* BufferListener methods */
wenzelm@34318
   224
immler@34545
   225
  private var changes: List[Text.Change] = Nil
immler@34545
   226
immler@34547
   227
  private def commit: Unit = synchronized {
immler@34545
   228
    if (col != null) {
immler@34574
   229
      def split_changes(c: Text.Change): List[Text.Change] = {
wenzelm@34582
   230
        val MAX = TheoryView.MAX_CHANGE_LENGTH
wenzelm@34582
   231
        if (c.added.length <= MAX) List(c)
wenzelm@34582
   232
        else Text.Change(c.id, c.start, c.added.substring(0, MAX), c.removed) ::
wenzelm@34582
   233
          split_changes(new Text.Change(id(), c.start + MAX, c.added.substring(MAX), c.removed))
immler@34574
   234
      }
immler@34574
   235
      val new_changes = split_changes(col)
immler@34574
   236
      changes = new_changes.reverse ::: changes
immler@34574
   237
      new_changes map (document_actor ! _)
immler@34545
   238
    }
wenzelm@34318
   239
    col = null
wenzelm@34446
   240
    if (col_timer.isRunning())
wenzelm@34446
   241
      col_timer.stop()
wenzelm@34446
   242
  }
wenzelm@34446
   243
immler@34515
   244
  private def delay_commit {
wenzelm@34446
   245
    if (col_timer.isRunning())
wenzelm@34446
   246
      col_timer.restart()
wenzelm@34318
   247
    else
wenzelm@34446
   248
      col_timer.start()
wenzelm@34318
   249
  }
wenzelm@34446
   250
wenzelm@34446
   251
wenzelm@34446
   252
  override def contentInserted(buffer: JEditBuffer,
wenzelm@34446
   253
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34446
   254
wenzelm@34446
   255
  override def contentRemoved(buffer: JEditBuffer,
wenzelm@34446
   256
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34318
   257
wenzelm@34446
   258
  override def preContentInserted(buffer: JEditBuffer,
wenzelm@34588
   259
    start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34446
   260
  {
immler@34526
   261
    val text = buffer.getText(offset, length)
immler@34364
   262
    if (col == null)
immler@34541
   263
      col = new Text.Change(id(), offset, text, 0)
immler@34526
   264
    else if (col.start <= offset && offset <= col.start + col.added.length)
immler@34541
   265
      col = new Text.Change(col.id, col.start, col.added + text, col.removed)
wenzelm@34446
   266
    else {
immler@34515
   267
      commit
immler@34541
   268
      col = new Text.Change(id(), offset, text, 0)
wenzelm@34318
   269
    }
immler@34515
   270
    delay_commit
wenzelm@34446
   271
  }
wenzelm@34446
   272
wenzelm@34446
   273
  override def preContentRemoved(buffer: JEditBuffer,
wenzelm@34588
   274
    start_line: Int, start: Int, num_lines: Int, removed: Int)
wenzelm@34446
   275
  {
wenzelm@34318
   276
    if (col == null)
immler@34541
   277
      col = new Text.Change(id(), start, "", removed)
immler@34526
   278
    else if (col.start > start + removed || start > col.start + col.added.length) {
immler@34515
   279
      commit
immler@34541
   280
      col = new Text.Change(id(), start, "", removed)
wenzelm@34318
   281
    }
wenzelm@34318
   282
    else {
immler@34526
   283
/*      val offset = start - col.start
immler@34526
   284
      val diff = col.added.length - removed
wenzelm@34446
   285
      val (added, add_removed) =
wenzelm@34446
   286
        if (diff < offset)
wenzelm@34318
   287
          (offset max 0, diff - (offset max 0))
wenzelm@34446
   288
        else
wenzelm@34318
   289
          (diff - (offset min 0), offset min 0)
immler@34526
   290
      col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
immler@34526
   291
      commit
immler@34541
   292
      col = new Text.Change(id(), start, "", removed)
wenzelm@34318
   293
    }
immler@34515
   294
    delay_commit
wenzelm@34318
   295
  }
wenzelm@34318
   296
wenzelm@34446
   297
  override def bufferLoaded(buffer: JEditBuffer) { }
wenzelm@34446
   298
  override def foldHandlerChanged(buffer: JEditBuffer) { }
wenzelm@34446
   299
  override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
wenzelm@34446
   300
  override def transactionComplete(buffer: JEditBuffer) { }
wenzelm@34588
   301
wenzelm@34447
   302
}