src/Tools/jEdit/src/jedit/TheoryView.scala
author immler@in.tum.de
Wed Jul 08 15:15:15 2009 +0200 (2009-07-08)
changeset 34653 2e033aaf128e
parent 34652 5fe5e00ec430
child 34654 30f588245884
permissions -rw-r--r--
commands carrying state-information
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
immler@34653
    14
import isabelle.proofdocument.{ProofDocument, Text}
immler@34649
    15
import isabelle.prover.{Prover, ProverEvents, 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}
immler@34649
    25
import org.gjt.sp.jedit.syntax.{ModeProvider, 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
  
immler@34653
    33
  def choose_color(cmd: Command, doc: ProofDocument): Color = {
immler@34653
    34
    cmd.status(doc) match {
immler@34653
    35
      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
immler@34653
    36
      case Command.Status.FINISHED => new Color(234, 248, 255)
immler@34653
    37
      case Command.Status.FAILED => new Color(255, 192, 192)
immler@34653
    38
      case _ => Color.red
immler@34653
    39
    }
wenzelm@34318
    40
  }
wenzelm@34318
    41
}
wenzelm@34318
    42
wenzelm@34446
    43
immler@34532
    44
class TheoryView (text_area: JEditTextArea, document_actor: Actor)
wenzelm@34588
    45
    extends TextAreaExtension with BufferListener
wenzelm@34588
    46
{
immler@34406
    47
wenzelm@34603
    48
  def id() = Isabelle.system.id()
immler@34541
    49
  
wenzelm@34446
    50
  private val buffer = text_area.getBuffer
immler@34475
    51
  private val prover = Isabelle.prover_setup(buffer).get.prover
wenzelm@34446
    52
wenzelm@34446
    53
immler@34526
    54
  private var col: Text.Change = null
immler@34650
    55
  private var doc_id: IsarDocument.Document_ID = prover.document(null).id
immler@34650
    56
  def current_document() = prover.document(doc_id)
wenzelm@34446
    57
wenzelm@34446
    58
  private val col_timer = new Timer(300, new ActionListener() {
immler@34515
    59
    override def actionPerformed(e: ActionEvent) = commit
wenzelm@34318
    60
  })
immler@34406
    61
wenzelm@34446
    62
  col_timer.stop
wenzelm@34446
    63
  col_timer.setRepeats(true)
wenzelm@34446
    64
wenzelm@34446
    65
immler@34566
    66
  private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current)
wenzelm@34446
    67
wenzelm@34318
    68
wenzelm@34446
    69
  /* activation */
wenzelm@34446
    70
wenzelm@34446
    71
  private val selected_state_controller = new CaretListener {
wenzelm@34446
    72
    override def caretUpdate(e: CaretEvent) = {
immler@34650
    73
      val doc = current_document()
immler@34554
    74
      val cmd = doc.find_command_at(e.getDot)
immler@34554
    75
      if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
immler@34475
    76
          Isabelle.prover_setup(buffer).get.selected_state != cmd)
immler@34475
    77
        Isabelle.prover_setup(buffer).get.selected_state = cmd
wenzelm@34318
    78
    }
wenzelm@34318
    79
  }
wenzelm@34318
    80
wenzelm@34582
    81
  def activate() {
wenzelm@34446
    82
    text_area.addCaretListener(selected_state_controller)
wenzelm@34446
    83
    text_area.addLeftOfScrollBar(phase_overview)
wenzelm@34446
    84
    text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
immler@34538
    85
    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
immler@34649
    86
    buffer.addBufferListener(this)
immler@34649
    87
immler@34650
    88
    col = Text.Change(doc_id, Isabelle.system.id(), 0,
immler@34650
    89
      buffer.getText(0, buffer.getLength), "")
immler@34650
    90
    commit
wenzelm@34446
    91
  }
wenzelm@34446
    92
wenzelm@34582
    93
  def deactivate() {
immler@34649
    94
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
immler@34649
    95
    buffer.removeBufferListener(this)
wenzelm@34446
    96
    text_area.getPainter.removeExtension(this)
wenzelm@34446
    97
    text_area.removeLeftOfScrollBar(phase_overview)
wenzelm@34446
    98
    text_area.removeCaretListener(selected_state_controller)
wenzelm@34446
    99
  }
wenzelm@34446
   100
wenzelm@34446
   101
wenzelm@34446
   102
  /* painting */
wenzelm@34446
   103
wenzelm@34643
   104
  val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() }
wenzelm@34643
   105
  val repaint_delay = Swing_Thread.delay(100){ repaint_all() }
immler@34538
   106
  
wenzelm@34582
   107
  val change_receiver = actor {
wenzelm@34582
   108
    loop {
wenzelm@34582
   109
      react {
immler@34649
   110
        case ProverEvents.Activate =>
immler@34649
   111
          activate()
immler@34649
   112
        case c: Command =>
wenzelm@34643
   113
          update_delay()
wenzelm@34643
   114
          repaint_delay()
wenzelm@34643
   115
          phase_overview.repaint_delay()
immler@34649
   116
        case x => System.err.println("warning: change_receiver ignored " + x)
immler@34538
   117
      }
immler@34538
   118
    }
wenzelm@34583
   119
  }
wenzelm@34446
   120
immler@34545
   121
  def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int =
immler@34545
   122
    changes match {
immler@34545
   123
      case Nil => pos
immler@34650
   124
      case Text.Change(_, id, start, added, removed) :: rest_changes => {
wenzelm@34582
   125
        val shifted =
wenzelm@34582
   126
          if (start <= pos)
immler@34545
   127
            if (pos < start + added.length) start
immler@34648
   128
            else pos - added.length + removed.length
immler@34545
   129
          else pos
immler@34547
   130
        if (id == to_id) pos
immler@34545
   131
        else _from_current(to_id, rest_changes, shifted)
immler@34545
   132
      }
immler@34545
   133
    }
wenzelm@34446
   134
immler@34545
   135
  def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int =
immler@34545
   136
    changes match {
immler@34545
   137
      case Nil => pos
immler@34650
   138
      case Text.Change(_, id, start, added, removed) :: rest_changes => {
immler@34547
   139
        val shifted = _to_current(from_id, rest_changes, pos)
immler@34547
   140
        if (id == from_id) pos
immler@34547
   141
        else if (start <= shifted) {
immler@34648
   142
          if (shifted < start + removed.length) start
immler@34648
   143
          else shifted + added.length - removed.length
immler@34547
   144
        } else shifted
immler@34545
   145
      }
immler@34545
   146
    }
immler@34545
   147
immler@34651
   148
  def to_current(from_id: String, pos: Int) = _to_current(from_id,
immler@34651
   149
    if (col == null) current_changes else col :: current_changes, pos)
immler@34651
   150
  def from_current(to_id: String, pos: Int) = _from_current(to_id,
immler@34651
   151
    if (col == null) current_changes else col :: current_changes, pos)
immler@34651
   152
  def to_current(doc: isabelle.proofdocument.ProofDocument, pos: Int): Int =
immler@34651
   153
    to_current(doc.id, pos)
immler@34651
   154
  def from_current(doc: isabelle.proofdocument.ProofDocument, pos: Int): Int =
immler@34651
   155
    from_current(doc.id, pos)
immler@34651
   156
immler@34651
   157
  /* update to desired version */
immler@34651
   158
immler@34651
   159
  def set_version(id: String) {
immler@34651
   160
    // changes in buffer must be ignored
immler@34651
   161
    buffer.removeBufferListener(this)
immler@34652
   162
immler@34652
   163
    val base = changes.find(_.id == doc_id).get
immler@34652
   164
    val goal = changes.find(_.id == id).get
immler@34652
   165
immler@34652
   166
    if (changes.indexOf(base) < changes.indexOf(goal))
immler@34652
   167
      changes.dropWhile(_ != base).takeWhile(_ != goal).map { c =>
immler@34652
   168
        buffer.remove(c.start, c.added.length)
immler@34652
   169
        buffer.insert(c.start, c.removed)}
immler@34652
   170
    else
immler@34652
   171
      changes.dropWhile(_ != goal).takeWhile(_ != base).reverse.map { c =>
immler@34652
   172
        buffer.remove(c.start, c.removed.length)
immler@34652
   173
        buffer.insert(c.start, c.added)}
immler@34652
   174
immler@34652
   175
    val content = buffer.getText(0, buffer.getLength)
immler@34651
   176
    doc_id = id
immler@34653
   177
    // invoke repaint
immler@34653
   178
    update_delay()
immler@34653
   179
    repaint_delay()
immler@34653
   180
    phase_overview.repaint_delay()
immler@34653
   181
immler@34651
   182
    buffer.addBufferListener(this)
immler@34651
   183
  }
wenzelm@34446
   184
wenzelm@34446
   185
  def repaint(cmd: Command) =
wenzelm@34318
   186
  {
immler@34650
   187
    val document = current_document()
wenzelm@34507
   188
    if (text_area != null) {
immler@34554
   189
      val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document)))
immler@34554
   190
      val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1)
immler@34406
   191
      text_area.invalidateLineRange(start, stop)
wenzelm@34446
   192
immler@34475
   193
      if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
immler@34475
   194
        Isabelle.prover_setup(buffer).get.selected_state = cmd  // update State view
wenzelm@34318
   195
    }
wenzelm@34318
   196
  }
wenzelm@34446
   197
wenzelm@34588
   198
  def repaint_all()
wenzelm@34318
   199
  {
immler@34406
   200
    if (text_area != null)
wenzelm@34446
   201
      text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
wenzelm@34318
   202
  }
immler@34391
   203
wenzelm@34446
   204
  def encolor(gfx: Graphics2D,
wenzelm@34588
   205
    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
wenzelm@34446
   206
  {
wenzelm@34446
   207
    val start = text_area.offsetToXY(begin)
wenzelm@34446
   208
    val stop =
wenzelm@34446
   209
      if (finish < buffer.getLength) text_area.offsetToXY(finish)
wenzelm@34446
   210
      else {
wenzelm@34446
   211
        val p = text_area.offsetToXY(finish - 1)
immler@34515
   212
        val metrics = text_area.getPainter.getFontMetrics
immler@34515
   213
        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
wenzelm@34446
   214
        p
immler@34391
   215
      }
wenzelm@34446
   216
wenzelm@34446
   217
    if (start != null && stop != null) {
wenzelm@34446
   218
      gfx.setColor(color)
wenzelm@34446
   219
      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
wenzelm@34446
   220
      else gfx.drawRect(start.x, y, stop.x - start.x, height)
wenzelm@34446
   221
    }
immler@34391
   222
  }
immler@34391
   223
wenzelm@34446
   224
wenzelm@34446
   225
  /* TextAreaExtension methods */
wenzelm@34446
   226
wenzelm@34446
   227
  override def paintValidLine(gfx: Graphics2D,
wenzelm@34588
   228
    screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@34446
   229
  {
immler@34650
   230
    val document = current_document()
immler@34545
   231
    def from_current(pos: Int) = this.from_current(document.id, pos)
immler@34545
   232
    def to_current(pos: Int) = this.to_current(document.id, pos)
wenzelm@34446
   233
    val saved_color = gfx.getColor
wenzelm@34446
   234
wenzelm@34446
   235
    val metrics = text_area.getPainter.getFontMetrics
immler@34596
   236
immler@34596
   237
    // encolor phase
immler@34545
   238
    var e = document.find_command_at(from_current(start))
immler@34596
   239
    while (e != null && e.start(document) < end) {
immler@34554
   240
      val begin = start max to_current(e.start(document))
immler@34554
   241
      val finish = end - 1 min to_current(e.stop(document))
immler@34653
   242
      encolor(gfx, y, metrics.getHeight, begin, finish,
immler@34653
   243
        TheoryView.choose_color(e, document), true)
immler@34596
   244
      e = document.commands.next(e).getOrElse(null)
wenzelm@34318
   245
    }
immler@34391
   246
wenzelm@34446
   247
    gfx.setColor(saved_color)
wenzelm@34318
   248
  }
wenzelm@34446
   249
immler@34562
   250
  override def getToolTipText(x: Int, y: Int) = {
immler@34650
   251
    val document = current_document()
immler@34562
   252
    val offset = from_current(document.id, text_area.xyToOffset(x, y))
immler@34562
   253
    val cmd = document.find_command_at(offset)
immler@34562
   254
    if (cmd != null) {
immler@34562
   255
      document.token_start(cmd.tokens.first)
immler@34653
   256
      cmd.type_at(document, offset - cmd.start(document))
immler@34562
   257
    } else null
immler@34562
   258
  }
immler@34562
   259
wenzelm@34446
   260
  /* BufferListener methods */
wenzelm@34318
   261
immler@34545
   262
  private var changes: List[Text.Change] = Nil
immler@34651
   263
  private def current_changes = changes.dropWhile(_.id != doc_id)
immler@34652
   264
  def get_changes = changes
immler@34545
   265
immler@34547
   266
  private def commit: Unit = synchronized {
immler@34545
   267
    if (col != null) {
immler@34574
   268
      def split_changes(c: Text.Change): List[Text.Change] = {
wenzelm@34582
   269
        val MAX = TheoryView.MAX_CHANGE_LENGTH
wenzelm@34582
   270
        if (c.added.length <= MAX) List(c)
immler@34650
   271
        else Text.Change(c.base_id, c.id, c.start, c.added.substring(0, MAX), c.removed) ::
immler@34650
   272
          split_changes(new Text.Change(c.id, id(), c.start + MAX, c.added.substring(MAX), ""))
immler@34574
   273
      }
immler@34574
   274
      val new_changes = split_changes(col)
immler@34651
   275
      changes = new_changes.reverse ::: current_changes
immler@34651
   276
      doc_id = new_changes.head.id
immler@34574
   277
      new_changes map (document_actor ! _)
immler@34650
   278
      doc_id = new_changes.last.id
immler@34545
   279
    }
wenzelm@34318
   280
    col = null
wenzelm@34446
   281
    if (col_timer.isRunning())
wenzelm@34446
   282
      col_timer.stop()
wenzelm@34446
   283
  }
wenzelm@34446
   284
immler@34515
   285
  private def delay_commit {
wenzelm@34446
   286
    if (col_timer.isRunning())
wenzelm@34446
   287
      col_timer.restart()
wenzelm@34318
   288
    else
wenzelm@34446
   289
      col_timer.start()
wenzelm@34318
   290
  }
wenzelm@34446
   291
wenzelm@34446
   292
wenzelm@34446
   293
  override def contentInserted(buffer: JEditBuffer,
wenzelm@34446
   294
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34446
   295
wenzelm@34446
   296
  override def contentRemoved(buffer: JEditBuffer,
wenzelm@34446
   297
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34318
   298
wenzelm@34446
   299
  override def preContentInserted(buffer: JEditBuffer,
wenzelm@34588
   300
    start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34446
   301
  {
immler@34526
   302
    val text = buffer.getText(offset, length)
immler@34364
   303
    if (col == null)
immler@34650
   304
      col = new Text.Change(doc_id, id(), offset, text, "")
immler@34526
   305
    else if (col.start <= offset && offset <= col.start + col.added.length)
immler@34650
   306
      col = new Text.Change(doc_id, col.id, col.start, col.added + text, col.removed)
wenzelm@34446
   307
    else {
immler@34515
   308
      commit
immler@34650
   309
      col = new Text.Change(doc_id, id(), offset, text, "")
wenzelm@34318
   310
    }
immler@34515
   311
    delay_commit
wenzelm@34446
   312
  }
wenzelm@34446
   313
wenzelm@34446
   314
  override def preContentRemoved(buffer: JEditBuffer,
immler@34648
   315
    start_line: Int, start: Int, num_lines: Int, removed_length: Int)
wenzelm@34446
   316
  {
immler@34648
   317
    val removed = buffer.getText(start, removed_length)
wenzelm@34318
   318
    if (col == null)
immler@34650
   319
      col = new Text.Change(doc_id, id(), start, "", removed)
immler@34648
   320
    else if (col.start > start + removed_length || start > col.start + col.added.length) {
immler@34515
   321
      commit
immler@34650
   322
      col = new Text.Change(doc_id, id(), start, "", removed)
wenzelm@34318
   323
    }
wenzelm@34318
   324
    else {
immler@34526
   325
/*      val offset = start - col.start
immler@34526
   326
      val diff = col.added.length - removed
wenzelm@34446
   327
      val (added, add_removed) =
wenzelm@34446
   328
        if (diff < offset)
wenzelm@34318
   329
          (offset max 0, diff - (offset max 0))
wenzelm@34446
   330
        else
wenzelm@34318
   331
          (diff - (offset min 0), offset min 0)
immler@34526
   332
      col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
immler@34526
   333
      commit
immler@34650
   334
      col = new Text.Change(doc_id, id(), start, "", removed)
wenzelm@34318
   335
    }
immler@34515
   336
    delay_commit
wenzelm@34318
   337
  }
wenzelm@34318
   338
wenzelm@34446
   339
  override def bufferLoaded(buffer: JEditBuffer) { }
wenzelm@34446
   340
  override def foldHandlerChanged(buffer: JEditBuffer) { }
wenzelm@34446
   341
  override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
wenzelm@34446
   342
  override def transactionComplete(buffer: JEditBuffer) { }
wenzelm@34588
   343
wenzelm@34447
   344
}