src/Tools/jEdit/src/jedit/TheoryView.scala
author wenzelm
Fri Dec 19 22:24:32 2008 +0100 (2008-12-19)
changeset 34407 aad6834ba380
parent 34406 f81cd75ae331
child 34408 ad7b6c4813c8
permissions -rw-r--r--
added some headers and comments;
wenzelm@34407
     1
/*
wenzelm@34407
     2
 * XML/CSS rendering -- user agent
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Fabian Immler, TU Munich
wenzelm@34407
     5
 * @author Johannes Hölzl, TU Munich
wenzelm@34407
     6
 */
wenzelm@34407
     7
wenzelm@34318
     8
package isabelle.jedit
wenzelm@34318
     9
wenzelm@34318
    10
import isabelle.utils.EventSource
wenzelm@34318
    11
wenzelm@34318
    12
import isabelle.proofdocument.Text
wenzelm@34318
    13
wenzelm@34318
    14
import isabelle.prover.{ Prover, Command, CommandChangeInfo }
wenzelm@34318
    15
import isabelle.prover.Command.Phase
wenzelm@34318
    16
wenzelm@34318
    17
import javax.swing.Timer
wenzelm@34318
    18
import javax.swing.event.{ CaretListener, CaretEvent }
wenzelm@34318
    19
import java.awt.Graphics2D
wenzelm@34318
    20
import java.awt.event.{ ActionEvent, ActionListener }
wenzelm@34318
    21
import java.awt.Color;
wenzelm@34318
    22
wenzelm@34318
    23
import org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer }
immler@34402
    24
import org.gjt.sp.jedit.textarea.{ JEditTextArea, TextAreaExtension, TextAreaPainter }
wenzelm@34318
    25
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@34318
    26
wenzelm@34318
    27
object TheoryView {
wenzelm@34318
    28
wenzelm@34318
    29
  def chooseColor(state : Command) : Color = {
wenzelm@34318
    30
    if (state == null)
wenzelm@34318
    31
      Color.red
wenzelm@34318
    32
    else
wenzelm@34318
    33
      state.phase match {
wenzelm@34318
    34
        case Phase.UNPROCESSED => new Color(255, 255, 192)
wenzelm@34318
    35
        case Phase.FINISHED => new Color(192, 255, 192)
wenzelm@34318
    36
        case Phase.FAILED => new Color(255, 192, 192)
wenzelm@34318
    37
        case _ => Color.red
wenzelm@34318
    38
      }
wenzelm@34318
    39
  }
immler@34391
    40
immler@34391
    41
  def chooseColor(status : String) : Color = {
immler@34391
    42
    //TODO: as properties!
immler@34391
    43
    status match {
immler@34399
    44
      //outer
immler@34399
    45
      case "ident" | "command" | "keyword" => Color.blue
immler@34399
    46
      case "verbatim"=> Color.green
immler@34399
    47
      case "comment" => Color.gray
immler@34399
    48
      case "control" => Color.white
immler@34399
    49
      case "malformed" => Color.red
immler@34399
    50
      case "string" | "altstring" => Color.orange
immler@34399
    51
      //logical
immler@34399
    52
      case "tclass" | "tycon" | "fixed_decl"  | "fixed"
immler@34399
    53
        | "const_decl" | "const" | "fact_decl" | "fact"
immler@34399
    54
        |"dynamic_fact" |"local_fact_decl" | "local_fact"
immler@34399
    55
        => new Color(255, 0, 255)
immler@34399
    56
      //inner syntax
immler@34399
    57
      case "tfree" | "free" => Color.blue
immler@34399
    58
      case "tvar" | "skolem" | "bound" | "var" => Color.green
immler@34399
    59
      case "num" | "xnum" | "xstr" | "literal" | "inner_comment" => new Color(255, 128, 128)
immler@34399
    60
      case "sort" | "typ" | "term" | "prop" | "attribute" | "method"  => Color.yellow
immler@34399
    61
        // embedded source
immler@34399
    62
      case "doc_source"  | "ML_source" | "ML_antic" | "doc_antiq" | "antiq"
immler@34399
    63
        => new Color(0, 192, 0)
immler@34399
    64
      case _ => Color.white
immler@34391
    65
    }
immler@34391
    66
  }
wenzelm@34318
    67
}
wenzelm@34318
    68
immler@34406
    69
class TheoryView (text_area : JEditTextArea)
wenzelm@34318
    70
    extends TextAreaExtension with Text with BufferListener {
wenzelm@34318
    71
  import TheoryView._
wenzelm@34318
    72
  import Text.Changed
immler@34406
    73
immler@34406
    74
  var col : Changed = null
immler@34406
    75
immler@34406
    76
  val buffer = text_area.getBuffer
immler@34406
    77
  buffer.addBufferListener(this)
wenzelm@34318
    78
  
wenzelm@34318
    79
  val colTimer = new Timer(300, new ActionListener() {
wenzelm@34318
    80
    override def actionPerformed(e : ActionEvent) { commit() }
wenzelm@34318
    81
  })
wenzelm@34318
    82
  
wenzelm@34318
    83
  val changesSource = new EventSource[Changed]
immler@34406
    84
  val phase_overview = new PhaseOverviewPanel(Plugin.prover(buffer))
immler@34404
    85
immler@34404
    86
    val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll())
immler@34406
    87
    Plugin.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
wenzelm@34318
    88
    Plugin.plugin.viewFontChanged.add(font => updateFont())
immler@34406
    89
wenzelm@34318
    90
    colTimer.stop
wenzelm@34318
    91
    colTimer.setRepeats(true)
wenzelm@34318
    92
immler@34406
    93
  def activate() {
immler@34406
    94
    text_area.addCaretListener(selectedStateController)
immler@34406
    95
    phase_overview.textarea = text_area
immler@34406
    96
    text_area.addLeftOfScrollBar(phase_overview)
immler@34406
    97
    val painter = text_area.getPainter()
wenzelm@34318
    98
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
wenzelm@34318
    99
    updateFont()
wenzelm@34318
   100
  }
wenzelm@34318
   101
  
wenzelm@34318
   102
  private def updateFont() {
immler@34406
   103
    if (text_area != null) {
immler@34406
   104
      val painter = text_area.getPainter()
wenzelm@34318
   105
      if (Plugin.plugin.viewFont != null) {
wenzelm@34318
   106
        painter.setStyles(painter.getStyles().map(style =>
wenzelm@34318
   107
          new SyntaxStyle(style.getForegroundColor, 
wenzelm@34318
   108
                          style.getBackgroundColor, 
wenzelm@34318
   109
                          Plugin.plugin.viewFont)
wenzelm@34318
   110
        ))
wenzelm@34318
   111
        painter.setFont(Plugin.plugin.viewFont)
wenzelm@34318
   112
        repaintAll()
wenzelm@34318
   113
      }
wenzelm@34318
   114
    }
wenzelm@34318
   115
  }
wenzelm@34318
   116
  
immler@34406
   117
  def deactivate() {
immler@34406
   118
    text_area.getPainter().removeExtension(this)
immler@34406
   119
    text_area.removeCaretListener(selectedStateController)
immler@34406
   120
    text_area.removeLeftOfScrollBar(phase_overview)
wenzelm@34318
   121
  }
wenzelm@34318
   122
  
wenzelm@34318
   123
  val selectedStateController = new CaretListener() {
wenzelm@34318
   124
    override def caretUpdate(e : CaretEvent) {
immler@34406
   125
      val cmd = Plugin.prover(buffer).document.getNextCommandContaining(e.getDot())
wenzelm@34318
   126
      if (cmd != null && cmd.start <= e.getDot() && 
immler@34406
   127
            Plugin.prover_setup(buffer).selectedState != cmd)
immler@34406
   128
        Plugin.prover_setup(buffer).selectedState = cmd
wenzelm@34318
   129
    }
wenzelm@34318
   130
  }
wenzelm@34318
   131
wenzelm@34318
   132
  private def fromCurrent(pos : Int) =
wenzelm@34318
   133
    if (col != null && col.start <= pos)
wenzelm@34318
   134
      if (pos < col.start + col.added) col.start
wenzelm@34318
   135
      else pos - col.added + col.removed
wenzelm@34318
   136
    else pos
wenzelm@34318
   137
  
wenzelm@34318
   138
  private def toCurrent(pos : Int) = 
wenzelm@34318
   139
    if (col != null && col.start <= pos)
wenzelm@34318
   140
      if (pos < col.start + col.removed) col.start
wenzelm@34318
   141
      else pos + col.added - col.removed
wenzelm@34318
   142
    else pos
wenzelm@34318
   143
  
wenzelm@34318
   144
  def repaint(cmd : Command)
wenzelm@34318
   145
  {
immler@34404
   146
    val ph = cmd.phase
immler@34406
   147
    if (text_area != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
immler@34406
   148
      var start = text_area.getLineOfOffset(toCurrent(cmd.start))
immler@34406
   149
      var stop = text_area.getLineOfOffset(toCurrent(cmd.stop) - 1)
immler@34406
   150
      text_area.invalidateLineRange(start, stop)
wenzelm@34318
   151
      
immler@34406
   152
      if (Plugin.prover_setup(buffer).selectedState == cmd)
immler@34406
   153
        Plugin.prover_setup(buffer).selectedState = cmd // update State view
wenzelm@34318
   154
    }
wenzelm@34318
   155
  }
wenzelm@34318
   156
  
wenzelm@34318
   157
  def repaintAll()
wenzelm@34318
   158
  {
immler@34406
   159
    if (text_area != null)
immler@34406
   160
      text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
immler@34406
   161
                                   text_area.getLastPhysicalLine)
wenzelm@34318
   162
  }
immler@34391
   163
immler@34399
   164
  def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color, fill : Boolean){
immler@34406
   165
      val fm = text_area.getPainter.getFontMetrics
immler@34406
   166
      val startP = text_area.offsetToXY(begin)
immler@34406
   167
      val stopP = if (finish < buffer.getLength()) text_area.offsetToXY(finish)
immler@34406
   168
                  else { var p = text_area.offsetToXY(finish - 1)
immler@34391
   169
                         p.x = p.x + fm.charWidth(' ')
immler@34391
   170
                         p }
immler@34391
   171
			
immler@34391
   172
      if (startP != null && stopP != null) {
immler@34391
   173
        gfx.setColor(color)
immler@34399
   174
        if(fill){gfx.fillRect(startP.x, y, stopP.x - startP.x, height)}
immler@34399
   175
        else {gfx.drawRect(startP.x, y, stopP.x - startP.x, height)}
immler@34391
   176
      }
immler@34391
   177
  }
immler@34391
   178
wenzelm@34318
   179
  override def paintValidLine(gfx : Graphics2D, screenLine : Int,
wenzelm@34318
   180
                              pl : Int, start : Int, end : Int, y : Int)
wenzelm@34318
   181
  {	
immler@34406
   182
    val fm = text_area.getPainter.getFontMetrics
immler@34391
   183
    var savedColor = gfx.getColor
immler@34406
   184
    var e = Plugin.prover(buffer).document.getNextCommandContaining(fromCurrent(start))
immler@34391
   185
immler@34391
   186
    //Encolor Phase
wenzelm@34318
   187
    while (e != null && toCurrent(e.start) < end) {
immler@34392
   188
      val begin =  start max toCurrent(e.start)
immler@34392
   189
      val finish = end - 1 min  toCurrent(e.stop)
immler@34399
   190
      encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e), true)
immler@34391
   191
      // paint details of command
immler@34401
   192
      for(node <- e.root_node.dfs){
immler@34401
   193
        val begin = toCurrent(node.start + e.start)
immler@34401
   194
        val finish = toCurrent(node.end + e.start)
immler@34392
   195
        if(finish > start && begin < end)
immler@34400
   196
        encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node.short), true)
wenzelm@34318
   197
      }
wenzelm@34318
   198
      e = e.next
wenzelm@34318
   199
    }
immler@34391
   200
wenzelm@34318
   201
    gfx.setColor(savedColor)
wenzelm@34318
   202
  }
wenzelm@34318
   203
	
wenzelm@34318
   204
  def content(start : Int, stop : Int) = buffer.getText(start, stop - start)
immler@34406
   205
  override def length = buffer.getLength
wenzelm@34318
   206
wenzelm@34318
   207
  def changes = changesSource
wenzelm@34318
   208
wenzelm@34318
   209
  private def commit() {
wenzelm@34318
   210
    if (col != null)
wenzelm@34318
   211
      changes.fire(col)
wenzelm@34318
   212
    col = null
wenzelm@34318
   213
    if (colTimer.isRunning())
wenzelm@34318
   214
      colTimer.stop()
wenzelm@34318
   215
  }	
wenzelm@34318
   216
	
wenzelm@34318
   217
  private def delayCommit() {
wenzelm@34318
   218
    if (colTimer.isRunning())
wenzelm@34318
   219
      colTimer.restart()
wenzelm@34318
   220
    else
wenzelm@34318
   221
      colTimer.start()
wenzelm@34318
   222
  }
wenzelm@34318
   223
	
wenzelm@34318
   224
  override def contentInserted(buffer : JEditBuffer, startLine : Int, 
immler@34387
   225
                               offset : Int, numLines : Int, length : Int) { }
wenzelm@34318
   226
  override def contentRemoved(buffer : JEditBuffer, startLine : Int, 
wenzelm@34318
   227
                              offset : Int, numLines : Int, length : Int) { }
wenzelm@34318
   228
wenzelm@34318
   229
  override def preContentInserted(buffer : JEditBuffer, startLine : Int,
wenzelm@34318
   230
			offset : Int, numLines : Int, length : Int) {
immler@34364
   231
    if (col == null)
wenzelm@34318
   232
      col = new Changed(offset, length, 0)
wenzelm@34318
   233
    else if (col.start <= offset && offset <= col.start + col.added) 
wenzelm@34318
   234
      col = new Changed(col.start, col.added + length, col.removed)
wenzelm@34318
   235
    else { 
wenzelm@34318
   236
      commit()
wenzelm@34318
   237
      col = new Changed(offset, length, 0) 
wenzelm@34318
   238
    }
wenzelm@34318
   239
    delayCommit()
wenzelm@34318
   240
  }	
wenzelm@34318
   241
  
wenzelm@34318
   242
  override def preContentRemoved(buffer : JEditBuffer, startLine : Int,
wenzelm@34318
   243
			start : Int, numLines : Int, removed : Int) {
wenzelm@34318
   244
    if (col == null)
wenzelm@34318
   245
      col = new Changed(start, 0, removed)
wenzelm@34318
   246
    else if (col.start > start + removed || start > col.start + col.added) { 
wenzelm@34318
   247
      commit()
wenzelm@34318
   248
      col = new Changed(start, 0, removed) 
wenzelm@34318
   249
    }
wenzelm@34318
   250
    else {
wenzelm@34318
   251
      val offset = start - col.start
wenzelm@34318
   252
      val diff = col.added - removed
wenzelm@34318
   253
      val (added, addRemoved) = 
wenzelm@34318
   254
        if (diff < offset) 
wenzelm@34318
   255
          (offset max 0, diff - (offset max 0))
wenzelm@34318
   256
        else 
wenzelm@34318
   257
          (diff - (offset min 0), offset min 0)
wenzelm@34318
   258
      
wenzelm@34318
   259
      col = new Changed(start min col.start, added, col.removed - addRemoved) 
wenzelm@34318
   260
    }
wenzelm@34318
   261
    delayCommit()
wenzelm@34318
   262
  }
wenzelm@34318
   263
wenzelm@34318
   264
  override def bufferLoaded(buffer : JEditBuffer) { }
wenzelm@34318
   265
  override def foldHandlerChanged(buffer : JEditBuffer) { }
wenzelm@34318
   266
  override def foldLevelChanged(buffer : JEditBuffer, startLine : Int, 
wenzelm@34318
   267
                                endLine : Int) = { }
wenzelm@34318
   268
  override def transactionComplete(buffer : JEditBuffer) = { } 
wenzelm@34318
   269
}