src/Tools/jEdit/src/jedit/TheoryView.scala
author wenzelm
Sun Dec 28 19:26:18 2008 +0100 (2008-12-28)
changeset 34447 dc8b486fde9f
parent 34446 5c79f97ec1d1
child 34448 39cb4ed5183b
permissions -rw-r--r--
tuned;
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@34446
    11
wenzelm@34318
    12
import isabelle.utils.EventSource
wenzelm@34318
    13
import isabelle.proofdocument.Text
wenzelm@34446
    14
import isabelle.prover.{Prover, Command, CommandChangeInfo}
wenzelm@34318
    15
import isabelle.prover.Command.Phase
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@34318
    28
object TheoryView {
wenzelm@34318
    29
wenzelm@34446
    30
  def choose_color(state: Command): Color = {
wenzelm@34318
    31
    if (state == null)
wenzelm@34318
    32
      Color.red
wenzelm@34318
    33
    else
wenzelm@34318
    34
      state.phase match {
wenzelm@34318
    35
        case Phase.UNPROCESSED => new Color(255, 255, 192)
wenzelm@34318
    36
        case Phase.FINISHED => new Color(192, 255, 192)
wenzelm@34318
    37
        case Phase.FAILED => new Color(255, 192, 192)
wenzelm@34318
    38
        case _ => Color.red
wenzelm@34318
    39
      }
wenzelm@34318
    40
  }
immler@34391
    41
wenzelm@34446
    42
  def choose_color(markup: String): Color = {
wenzelm@34446
    43
    // TODO: as properties
wenzelm@34446
    44
    markup match {
wenzelm@34445
    45
      // logical entities
wenzelm@34445
    46
      case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
wenzelm@34445
    47
        | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
wenzelm@34445
    48
        | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255)
wenzelm@34445
    49
      // inner syntax
wenzelm@34445
    50
      case Markup.TFREE | Markup.FREE => Color.blue
wenzelm@34445
    51
      case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green
wenzelm@34445
    52
      case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
wenzelm@34445
    53
        | Markup.INNER_COMMENT => new Color(255, 128, 128)
wenzelm@34445
    54
      case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
wenzelm@34446
    55
        | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow
wenzelm@34445
    56
      // embedded source text
wenzelm@34445
    57
      case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
wenzelm@34445
    58
        | Markup.DOC_ANTIQ => new Color(0, 192, 0)
wenzelm@34445
    59
      // outer syntax
wenzelm@34445
    60
      case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue
wenzelm@34445
    61
      case Markup.VERBATIM => Color.green
wenzelm@34445
    62
      case Markup.COMMENT => Color.gray
wenzelm@34445
    63
      case Markup.CONTROL => Color.white
wenzelm@34445
    64
      case Markup.MALFORMED => Color.red
wenzelm@34445
    65
      case Markup.STRING | Markup.ALTSTRING => Color.orange
wenzelm@34445
    66
      // other
immler@34399
    67
      case _ => Color.white
immler@34391
    68
    }
immler@34391
    69
  }
wenzelm@34318
    70
}
wenzelm@34318
    71
wenzelm@34446
    72
wenzelm@34446
    73
class TheoryView (text_area: JEditTextArea)
wenzelm@34318
    74
    extends TextAreaExtension with Text with BufferListener {
immler@34406
    75
wenzelm@34446
    76
  private val buffer = text_area.getBuffer
immler@34406
    77
  buffer.addBufferListener(this)
wenzelm@34446
    78
wenzelm@34446
    79
wenzelm@34446
    80
  private var col: Text.Changed = null
wenzelm@34446
    81
wenzelm@34446
    82
  private val col_timer = new Timer(300, new ActionListener() {
wenzelm@34446
    83
    override def actionPerformed(e: ActionEvent) = commit()
wenzelm@34318
    84
  })
immler@34406
    85
wenzelm@34446
    86
  col_timer.stop
wenzelm@34446
    87
  col_timer.setRepeats(true)
wenzelm@34446
    88
wenzelm@34446
    89
wenzelm@34446
    90
  private val changes_source = new EventSource[Text.Changed]
wenzelm@34446
    91
  private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
wenzelm@34446
    92
wenzelm@34318
    93
wenzelm@34446
    94
  /* activation */
wenzelm@34446
    95
wenzelm@34446
    96
  Isabelle.plugin.font_changed.add(font => update_font())
wenzelm@34446
    97
wenzelm@34446
    98
  private def update_font() = {
immler@34406
    99
    if (text_area != null) {
wenzelm@34440
   100
      if (Isabelle.plugin.font != null) {
wenzelm@34446
   101
        val painter = text_area.getPainter
wenzelm@34434
   102
        painter.setStyles(painter.getStyles.map(style =>
wenzelm@34446
   103
          new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font)
wenzelm@34318
   104
        ))
wenzelm@34440
   105
        painter.setFont(Isabelle.plugin.font)
wenzelm@34446
   106
        repaint_all()
wenzelm@34318
   107
      }
wenzelm@34318
   108
    }
wenzelm@34318
   109
  }
wenzelm@34446
   110
wenzelm@34446
   111
  private val selected_state_controller = new CaretListener {
wenzelm@34446
   112
    override def caretUpdate(e: CaretEvent) = {
wenzelm@34446
   113
      val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
wenzelm@34446
   114
      if (cmd != null && cmd.start <= e.getDot &&
wenzelm@34446
   115
          Isabelle.prover_setup(buffer).selectedState != cmd)
wenzelm@34440
   116
        Isabelle.prover_setup(buffer).selectedState = cmd
wenzelm@34318
   117
    }
wenzelm@34318
   118
  }
wenzelm@34318
   119
wenzelm@34446
   120
  def activate() = {
wenzelm@34446
   121
    text_area.addCaretListener(selected_state_controller)
wenzelm@34446
   122
    phase_overview.textarea = text_area
wenzelm@34446
   123
    text_area.addLeftOfScrollBar(phase_overview)
wenzelm@34446
   124
    text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
wenzelm@34446
   125
    update_font()
wenzelm@34446
   126
  }
wenzelm@34446
   127
wenzelm@34446
   128
  def deactivate() = {
wenzelm@34446
   129
    text_area.getPainter.removeExtension(this)
wenzelm@34446
   130
    text_area.removeLeftOfScrollBar(phase_overview)
wenzelm@34446
   131
    text_area.removeCaretListener(selected_state_controller)
wenzelm@34446
   132
  }
wenzelm@34446
   133
wenzelm@34446
   134
wenzelm@34446
   135
  /* painting */
wenzelm@34446
   136
wenzelm@34446
   137
  val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
wenzelm@34446
   138
  Isabelle.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
wenzelm@34446
   139
wenzelm@34446
   140
  private def from_current(pos: Int) =
wenzelm@34318
   141
    if (col != null && col.start <= pos)
wenzelm@34318
   142
      if (pos < col.start + col.added) col.start
wenzelm@34318
   143
      else pos - col.added + col.removed
wenzelm@34318
   144
    else pos
wenzelm@34446
   145
wenzelm@34446
   146
  private def to_current(pos : Int) =
wenzelm@34318
   147
    if (col != null && col.start <= pos)
wenzelm@34318
   148
      if (pos < col.start + col.removed) col.start
wenzelm@34318
   149
      else pos + col.added - col.removed
wenzelm@34318
   150
    else pos
wenzelm@34446
   151
wenzelm@34446
   152
  def repaint(cmd: Command) =
wenzelm@34318
   153
  {
wenzelm@34446
   154
    val phase = cmd.phase
wenzelm@34446
   155
    if (text_area != null && phase != Phase.REMOVE && phase != Phase.REMOVED) {
wenzelm@34446
   156
      val start = text_area.getLineOfOffset(to_current(cmd.start))
wenzelm@34446
   157
      val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
immler@34406
   158
      text_area.invalidateLineRange(start, stop)
wenzelm@34446
   159
wenzelm@34440
   160
      if (Isabelle.prover_setup(buffer).selectedState == cmd)
wenzelm@34446
   161
        Isabelle.prover_setup(buffer).selectedState = cmd  // update State view
wenzelm@34318
   162
    }
wenzelm@34318
   163
  }
wenzelm@34446
   164
wenzelm@34446
   165
  def repaint_all() =
wenzelm@34318
   166
  {
immler@34406
   167
    if (text_area != null)
wenzelm@34446
   168
      text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
wenzelm@34318
   169
  }
immler@34391
   170
wenzelm@34446
   171
  def encolor(gfx: Graphics2D,
wenzelm@34446
   172
    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) =
wenzelm@34446
   173
  {
wenzelm@34446
   174
    val start = text_area.offsetToXY(begin)
wenzelm@34446
   175
    val stop =
wenzelm@34446
   176
      if (finish < buffer.getLength) text_area.offsetToXY(finish)
wenzelm@34446
   177
      else {
wenzelm@34446
   178
        val p = text_area.offsetToXY(finish - 1)
wenzelm@34446
   179
        p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ')
wenzelm@34446
   180
        p
immler@34391
   181
      }
wenzelm@34446
   182
wenzelm@34446
   183
    if (start != null && stop != null) {
wenzelm@34446
   184
      gfx.setColor(color)
wenzelm@34446
   185
      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
wenzelm@34446
   186
      else gfx.drawRect(start.x, y, stop.x - start.x, height)
wenzelm@34446
   187
    }
immler@34391
   188
  }
immler@34391
   189
wenzelm@34446
   190
wenzelm@34446
   191
  /* TextAreaExtension methods */
wenzelm@34446
   192
wenzelm@34446
   193
  override def paintValidLine(gfx: Graphics2D,
wenzelm@34446
   194
    screen_line: Int, pl: Int, start: Int, end: Int, y: Int) =
wenzelm@34446
   195
  {
wenzelm@34446
   196
    val saved_color = gfx.getColor
wenzelm@34446
   197
wenzelm@34446
   198
    val metrics = text_area.getPainter.getFontMetrics
wenzelm@34446
   199
    var e = Isabelle.prover(buffer).document.getNextCommandContaining(from_current(start))
immler@34391
   200
wenzelm@34446
   201
    // encolor phase
wenzelm@34446
   202
    while (e != null && to_current(e.start) < end) {
wenzelm@34446
   203
      val begin = start max to_current(e.start)
wenzelm@34446
   204
      val finish = end - 1 min to_current(e.stop)
wenzelm@34446
   205
      encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
wenzelm@34446
   206
immler@34391
   207
      // paint details of command
wenzelm@34446
   208
      for (node <- e.root_node.dfs) {
wenzelm@34446
   209
        val begin = to_current(node.start + e.start)
wenzelm@34446
   210
        val finish = to_current(node.end + e.start)
wenzelm@34446
   211
        if (finish > start && begin < end) {
wenzelm@34446
   212
          encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end,
wenzelm@34446
   213
            TheoryView.choose_color(node.short), true)
wenzelm@34446
   214
        }
wenzelm@34318
   215
      }
wenzelm@34318
   216
      e = e.next
wenzelm@34318
   217
    }
immler@34391
   218
wenzelm@34446
   219
    gfx.setColor(saved_color)
wenzelm@34318
   220
  }
wenzelm@34446
   221
wenzelm@34446
   222
wenzelm@34446
   223
  /* Text methods */
wenzelm@34318
   224
wenzelm@34446
   225
  def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
wenzelm@34446
   226
  def length = buffer.getLength
wenzelm@34446
   227
  def changes = changes_source
wenzelm@34446
   228
wenzelm@34446
   229
wenzelm@34446
   230
wenzelm@34446
   231
  /* BufferListener methods */
wenzelm@34318
   232
wenzelm@34318
   233
  private def commit() {
wenzelm@34318
   234
    if (col != null)
wenzelm@34318
   235
      changes.fire(col)
wenzelm@34318
   236
    col = null
wenzelm@34446
   237
    if (col_timer.isRunning())
wenzelm@34446
   238
      col_timer.stop()
wenzelm@34446
   239
  }
wenzelm@34446
   240
wenzelm@34446
   241
  private def delay_commit() {
wenzelm@34446
   242
    if (col_timer.isRunning())
wenzelm@34446
   243
      col_timer.restart()
wenzelm@34318
   244
    else
wenzelm@34446
   245
      col_timer.start()
wenzelm@34318
   246
  }
wenzelm@34446
   247
wenzelm@34446
   248
wenzelm@34446
   249
  override def contentInserted(buffer: JEditBuffer,
wenzelm@34446
   250
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34446
   251
wenzelm@34446
   252
  override def contentRemoved(buffer: JEditBuffer,
wenzelm@34446
   253
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
wenzelm@34318
   254
wenzelm@34446
   255
  override def preContentInserted(buffer: JEditBuffer,
wenzelm@34446
   256
    start_line: Int, offset: Int, num_lines: Int, length: Int) =
wenzelm@34446
   257
  {
immler@34364
   258
    if (col == null)
wenzelm@34446
   259
      col = new Text.Changed(offset, length, 0)
wenzelm@34446
   260
    else if (col.start <= offset && offset <= col.start + col.added)
wenzelm@34446
   261
      col = new Text.Changed(col.start, col.added + length, col.removed)
wenzelm@34446
   262
    else {
wenzelm@34318
   263
      commit()
wenzelm@34446
   264
      col = new Text.Changed(offset, length, 0)
wenzelm@34318
   265
    }
wenzelm@34446
   266
    delay_commit()
wenzelm@34446
   267
  }
wenzelm@34446
   268
wenzelm@34446
   269
  override def preContentRemoved(buffer: JEditBuffer,
wenzelm@34446
   270
    start_line: Int, start: Int, num_lines: Int, removed: Int) =
wenzelm@34446
   271
  {
wenzelm@34318
   272
    if (col == null)
wenzelm@34446
   273
      col = new Text.Changed(start, 0, removed)
wenzelm@34446
   274
    else if (col.start > start + removed || start > col.start + col.added) {
wenzelm@34318
   275
      commit()
wenzelm@34446
   276
      col = new Text.Changed(start, 0, removed)
wenzelm@34318
   277
    }
wenzelm@34318
   278
    else {
wenzelm@34318
   279
      val offset = start - col.start
wenzelm@34318
   280
      val diff = col.added - removed
wenzelm@34446
   281
      val (added, add_removed) =
wenzelm@34446
   282
        if (diff < offset)
wenzelm@34318
   283
          (offset max 0, diff - (offset max 0))
wenzelm@34446
   284
        else
wenzelm@34318
   285
          (diff - (offset min 0), offset min 0)
wenzelm@34446
   286
      col = new Text.Changed(start min col.start, added, col.removed - add_removed)
wenzelm@34318
   287
    }
wenzelm@34446
   288
    delay_commit()
wenzelm@34318
   289
  }
wenzelm@34318
   290
wenzelm@34446
   291
  override def bufferLoaded(buffer: JEditBuffer) { }
wenzelm@34446
   292
  override def foldHandlerChanged(buffer: JEditBuffer) { }
wenzelm@34446
   293
  override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
wenzelm@34446
   294
  override def transactionComplete(buffer: JEditBuffer) { }
wenzelm@34447
   295
}