src/Tools/jEdit/src/jedit/TheoryView.scala
author wenzelm
Tue Sep 15 18:14:28 2009 +0200 (2009-09-15)
changeset 34731 c0cb6bd10eec
parent 34724 b1079c3ba1da
child 34736 ff7734c8bdb7
permissions -rw-r--r--
keep BufferListener and TextAreaExtension private;
misc 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
wenzelm@34703
    11
import scala.actors.Actor, Actor._
wenzelm@34693
    12
import scala.collection.mutable
wenzelm@34446
    13
immler@34660
    14
import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
wenzelm@34719
    15
import isabelle.prover.{Prover, Command}
wenzelm@34318
    16
wenzelm@34703
    17
import java.awt.{Color, Graphics2D}
wenzelm@34447
    18
import javax.swing.event.{CaretListener, CaretEvent}
wenzelm@34318
    19
wenzelm@34446
    20
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
wenzelm@34446
    21
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
immler@34649
    22
import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
wenzelm@34318
    23
wenzelm@34446
    24
wenzelm@34588
    25
object TheoryView
wenzelm@34588
    26
{
wenzelm@34716
    27
  def choose_color(command: Command, doc: ProofDocument): Color =
wenzelm@34716
    28
  {
wenzelm@34716
    29
    command.status(doc) match {
immler@34653
    30
      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
immler@34653
    31
      case Command.Status.FINISHED => new Color(234, 248, 255)
wenzelm@34716
    32
      case Command.Status.FAILED => new Color(255, 106, 106)
immler@34653
    33
      case _ => Color.red
immler@34653
    34
    }
wenzelm@34318
    35
  }
wenzelm@34318
    36
}
wenzelm@34318
    37
wenzelm@34446
    38
wenzelm@34696
    39
class TheoryView(text_area: JEditTextArea)
wenzelm@34588
    40
{
wenzelm@34731
    41
  private val buffer = text_area.getBuffer
immler@34672
    42
wenzelm@34719
    43
wenzelm@34719
    44
  /* prover setup */
wenzelm@34719
    45
wenzelm@34724
    46
  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
wenzelm@34724
    47
wenzelm@34724
    48
  prover.command_change += ((command: Command) =>
wenzelm@34724
    49
    if (current_document().commands.contains(command))
wenzelm@34724
    50
      Swing_Thread.later {
wenzelm@34731
    51
        // FIXME proper handling of buffer vs. text areas
wenzelm@34724
    52
        // repaint if buffer is active
wenzelm@34724
    53
        if (text_area.getBuffer == buffer) {
wenzelm@34724
    54
          update_syntax(command)
wenzelm@34724
    55
          invalidate_line(command)
wenzelm@34724
    56
          phase_overview.repaint()
wenzelm@34719
    57
        }
wenzelm@34724
    58
      })
wenzelm@34731
    59
wenzelm@34731
    60
wenzelm@34731
    61
  /* changes vs. edits */
wenzelm@34731
    62
wenzelm@34731
    63
  private val change_0 = new Change(prover.document_0.id, None, Nil)
wenzelm@34731
    64
  private var _changes = List(change_0)   // owned by Swing/AWT thread
wenzelm@34731
    65
  def changes = _changes
wenzelm@34731
    66
  private var current_change = change_0
wenzelm@34731
    67
wenzelm@34731
    68
  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
wenzelm@34731
    69
wenzelm@34731
    70
  private val edits_delay = Swing_Thread.delay_last(300) {
wenzelm@34731
    71
    if (!edits.isEmpty) {
wenzelm@34731
    72
      val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
wenzelm@34731
    73
      _changes ::= change
wenzelm@34731
    74
      prover ! change
wenzelm@34731
    75
      current_change = change
wenzelm@34731
    76
      edits.clear
wenzelm@34731
    77
    }
wenzelm@34731
    78
  }
wenzelm@34731
    79
wenzelm@34731
    80
wenzelm@34731
    81
  /* buffer_listener */
wenzelm@34731
    82
wenzelm@34731
    83
  private val buffer_listener = new BufferListener {
wenzelm@34731
    84
    override def preContentInserted(buffer: JEditBuffer,
wenzelm@34731
    85
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34731
    86
    {
wenzelm@34731
    87
      edits += Insert(offset, buffer.getText(offset, length))
wenzelm@34731
    88
      edits_delay()
wenzelm@34731
    89
    }
wenzelm@34731
    90
wenzelm@34731
    91
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@34731
    92
      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
wenzelm@34731
    93
    {
wenzelm@34731
    94
      edits += Remove(start, buffer.getText(start, removed_length))
wenzelm@34731
    95
      edits_delay()
wenzelm@34731
    96
    }
wenzelm@34731
    97
wenzelm@34731
    98
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34731
    99
      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34731
   100
wenzelm@34731
   101
    override def contentRemoved(buffer: JEditBuffer,
wenzelm@34731
   102
      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34731
   103
wenzelm@34731
   104
    override def bufferLoaded(buffer: JEditBuffer) { }
wenzelm@34731
   105
    override def foldHandlerChanged(buffer: JEditBuffer) { }
wenzelm@34731
   106
    override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
wenzelm@34731
   107
    override def transactionComplete(buffer: JEditBuffer) { }
wenzelm@34731
   108
  }
wenzelm@34731
   109
wenzelm@34731
   110
wenzelm@34731
   111
  /* text_area_extension */
wenzelm@34731
   112
wenzelm@34731
   113
  private val text_area_extension = new TextAreaExtension {
wenzelm@34731
   114
    override def paintValidLine(gfx: Graphics2D,
wenzelm@34731
   115
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
wenzelm@34731
   116
    {
wenzelm@34731
   117
      val document = current_document()
wenzelm@34731
   118
      def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
wenzelm@34731
   119
      def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
wenzelm@34731
   120
      val saved_color = gfx.getColor
wenzelm@34731
   121
wenzelm@34731
   122
      val metrics = text_area.getPainter.getFontMetrics
wenzelm@34731
   123
wenzelm@34731
   124
      // encolor phase
wenzelm@34731
   125
      var cmd = document.command_at(from_current(start))
wenzelm@34731
   126
      while (cmd.isDefined && cmd.get.start(document) < end) {
wenzelm@34731
   127
        val e = cmd.get
wenzelm@34731
   128
        val begin = start max to_current(e.start(document))
wenzelm@34731
   129
        val finish = (end - 1) min to_current(e.stop(document))
wenzelm@34731
   130
        encolor(gfx, y, metrics.getHeight, begin, finish,
wenzelm@34731
   131
          TheoryView.choose_color(e, document), true)
wenzelm@34731
   132
        cmd = document.commands.next(e)
wenzelm@34731
   133
      }
wenzelm@34731
   134
wenzelm@34731
   135
      gfx.setColor(saved_color)
wenzelm@34731
   136
    }
wenzelm@34731
   137
wenzelm@34731
   138
    override def getToolTipText(x: Int, y: Int): String =
wenzelm@34731
   139
    {
wenzelm@34731
   140
      val document = current_document()
wenzelm@34731
   141
      val offset = from_current(document, text_area.xyToOffset(x, y))
wenzelm@34731
   142
      document.command_at(offset) match {
wenzelm@34731
   143
        case Some(cmd) =>
wenzelm@34731
   144
          document.token_start(cmd.tokens.first)
wenzelm@34731
   145
          cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
wenzelm@34731
   146
        case None => null
wenzelm@34731
   147
      }
wenzelm@34731
   148
    }
wenzelm@34731
   149
  }
wenzelm@34731
   150
wenzelm@34446
   151
immler@34680
   152
  /* activation */
wenzelm@34446
   153
immler@34566
   154
  private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current)
wenzelm@34446
   155
wenzelm@34446
   156
  private val selected_state_controller = new CaretListener {
wenzelm@34719
   157
    override def caretUpdate(e: CaretEvent) {
immler@34650
   158
      val doc = current_document()
wenzelm@34712
   159
      doc.command_at(e.getDot) match {
wenzelm@34712
   160
        case Some(cmd)
wenzelm@34712
   161
          if (doc.token_start(cmd.tokens.first) <= e.getDot &&
wenzelm@34712
   162
            Isabelle.plugin.selected_state != cmd) =>
wenzelm@34712
   163
          Isabelle.plugin.selected_state = cmd
wenzelm@34712
   164
        case _ =>
wenzelm@34712
   165
      }
wenzelm@34318
   166
    }
wenzelm@34318
   167
  }
wenzelm@34318
   168
wenzelm@34582
   169
  def activate() {
wenzelm@34446
   170
    text_area.addCaretListener(selected_state_controller)
wenzelm@34446
   171
    text_area.addLeftOfScrollBar(phase_overview)
wenzelm@34731
   172
    text_area.getPainter.
wenzelm@34731
   173
      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
immler@34538
   174
    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
wenzelm@34731
   175
    buffer.addBufferListener(buffer_listener)
immler@34671
   176
immler@34671
   177
    val dockable =
immler@34671
   178
      text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
immler@34671
   179
    if (dockable != null) {
immler@34671
   180
      val output_dockable = dockable.asInstanceOf[OutputDockable]
immler@34671
   181
      val output_text_view = prover.output_text_view
immler@34671
   182
      output_dockable.set_text(output_text_view)
immler@34671
   183
    }
immler@34671
   184
immler@34671
   185
    buffer.propertiesChanged()
wenzelm@34446
   186
  }
wenzelm@34446
   187
wenzelm@34582
   188
  def deactivate() {
immler@34649
   189
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
wenzelm@34731
   190
    buffer.removeBufferListener(buffer_listener)
wenzelm@34731
   191
    text_area.getPainter.removeExtension(text_area_extension)
wenzelm@34446
   192
    text_area.removeLeftOfScrollBar(phase_overview)
wenzelm@34446
   193
    text_area.removeCaretListener(selected_state_controller)
wenzelm@34446
   194
  }
wenzelm@34446
   195
wenzelm@34446
   196
wenzelm@34731
   197
  /* history of changes */
immler@34660
   198
immler@34660
   199
  private def doc_or_pred(c: Change): ProofDocument =
immler@34660
   200
    prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
wenzelm@34731
   201
immler@34654
   202
  def current_document() = doc_or_pred(current_change)
immler@34654
   203
wenzelm@34731
   204
immler@34654
   205
  /* update to desired version */
immler@34654
   206
immler@34660
   207
  def set_version(goal: Change) {
immler@34654
   208
    // changes in buffer must be ignored
wenzelm@34731
   209
    buffer.removeBufferListener(buffer_listener)
immler@34654
   210
wenzelm@34693
   211
    def apply(change: Change): Unit = change.edits.foreach {
wenzelm@34693
   212
      case Insert(start, text) => buffer.insert(start, text)
wenzelm@34693
   213
      case Remove(start, text) => buffer.remove(start, text.length)
immler@34660
   214
    }
immler@34660
   215
wenzelm@34693
   216
    def unapply(change: Change): Unit = change.edits.reverse.foreach {
wenzelm@34693
   217
      case Insert(start, text) => buffer.remove(start, text.length)
wenzelm@34693
   218
      case Remove(start, text) => buffer.insert(start, text)
immler@34660
   219
    }
wenzelm@34318
   220
immler@34654
   221
    // undo/redo changes
immler@34654
   222
    val ancs_current = current_change.ancestors
immler@34654
   223
    val ancs_goal = goal.ancestors
immler@34654
   224
    val paired = ancs_current.reverse zip ancs_goal.reverse
immler@34654
   225
    def last_common[A](xs: List[(A, A)]): Option[A] = {
immler@34654
   226
      xs match {
immler@34654
   227
        case (x, y) :: xs =>
immler@34654
   228
          if (x == y)
immler@34654
   229
            xs match {
immler@34654
   230
              case (a, b) :: ys =>
immler@34654
   231
                if (a == b) last_common(xs)
immler@34654
   232
                else Some(x)
immler@34654
   233
              case _ => Some(x)
immler@34654
   234
            }
immler@34654
   235
          else None
immler@34654
   236
        case _ => None
immler@34654
   237
      }
immler@34654
   238
    }
immler@34654
   239
    val common_anc = last_common(paired).get
immler@34654
   240
immler@34654
   241
    ancs_current.takeWhile(_ != common_anc) map unapply
immler@34654
   242
    ancs_goal.takeWhile(_ != common_anc).reverse map apply
immler@34654
   243
immler@34654
   244
    current_change = goal
immler@34654
   245
    // invoke repaint
immler@34679
   246
    buffer.propertiesChanged()
immler@34679
   247
    invalidate_all()
immler@34679
   248
    phase_overview.repaint()
immler@34654
   249
wenzelm@34703
   250
    // track changes in buffer
wenzelm@34731
   251
    buffer.addBufferListener(buffer_listener)
wenzelm@34318
   252
  }
wenzelm@34446
   253
wenzelm@34693
   254
immler@34680
   255
  /* transforming offsets */
immler@34680
   256
immler@34718
   257
  private def changes_from(doc: ProofDocument): List[Edit] =
immler@34718
   258
    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
immler@34718
   259
      edits.toList
immler@34680
   260
wenzelm@34695
   261
  def from_current(doc: ProofDocument, offset: Int): Int =
immler@34718
   262
    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
immler@34680
   263
wenzelm@34695
   264
  def to_current(doc: ProofDocument, offset: Int): Int =
immler@34718
   265
    (offset /: changes_from(doc)) ((i, change) => change after i)
immler@34680
   266
immler@34680
   267
immler@34680
   268
  private def lines_of_command(cmd: Command) =
immler@34680
   269
  {
immler@34680
   270
    val document = current_document()
immler@34681
   271
    (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
immler@34681
   272
     buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
immler@34680
   273
  }
immler@34680
   274
immler@34680
   275
immler@34680
   276
  /* (re)painting */
immler@34680
   277
wenzelm@34694
   278
  private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
immler@34680
   279
immler@34680
   280
  private def update_syntax(cmd: Command) {
immler@34680
   281
    val (line1, line2) = lines_of_command(cmd)
immler@34680
   282
    if (line2 >= text_area.getFirstLine &&
immler@34680
   283
      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
immler@34680
   284
        update_delay()
immler@34680
   285
  }
immler@34680
   286
immler@34680
   287
  private def invalidate_line(cmd: Command) =
immler@34680
   288
  {
immler@34680
   289
    val (start, stop) = lines_of_command(cmd)
immler@34680
   290
    text_area.invalidateLineRange(start, stop)
immler@34680
   291
immler@34680
   292
    if (Isabelle.plugin.selected_state == cmd)
immler@34680
   293
        Isabelle.plugin.selected_state = cmd  // update State view
immler@34680
   294
  }
immler@34680
   295
immler@34680
   296
  private def invalidate_all() =
immler@34680
   297
    text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
immler@34680
   298
      text_area.getLastPhysicalLine)
immler@34680
   299
immler@34680
   300
  private def encolor(gfx: Graphics2D,
immler@34680
   301
    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
immler@34680
   302
  {
immler@34680
   303
    val start = text_area.offsetToXY(begin)
immler@34680
   304
    val stop =
immler@34680
   305
      if (finish < buffer.getLength) text_area.offsetToXY(finish)
immler@34680
   306
      else {
immler@34680
   307
        val p = text_area.offsetToXY(finish - 1)
immler@34680
   308
        val metrics = text_area.getPainter.getFontMetrics
immler@34680
   309
        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
immler@34680
   310
        p
immler@34680
   311
      }
immler@34680
   312
immler@34680
   313
    if (start != null && stop != null) {
immler@34680
   314
      gfx.setColor(color)
immler@34680
   315
      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
immler@34680
   316
      else gfx.drawRect(start.x, y, stop.x - start.x, height)
immler@34680
   317
    }
immler@34680
   318
  }
immler@34680
   319
wenzelm@34696
   320
wenzelm@34719
   321
  /* init */
immler@34680
   322
wenzelm@34719
   323
  prover.start()
wenzelm@34719
   324
wenzelm@34719
   325
  edits += Insert(0, buffer.getText(0, buffer.getLength))
wenzelm@34719
   326
  edits_delay()
wenzelm@34447
   327
}