package isabelle.jedit
import isabelle.utils.EventSource
import isabelle.proofdocument.Text
import isabelle.prover.{ Prover, Command, CommandChangeInfo }
import isabelle.prover.Command.Phase
import javax.swing.Timer
import javax.swing.event.{ CaretListener, CaretEvent }
import java.awt.Graphics2D
import java.awt.event.{ ActionEvent, ActionListener }
import java.awt.Color;
import org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer }
import org.gjt.sp.jedit.textarea.{ TextArea, TextAreaExtension, TextAreaPainter }
import org.gjt.sp.jedit.syntax.SyntaxStyle
object TheoryView {
val ISABELLE_THEORY_PROPERTY = "de.tum.in.isabelle.jedit.Theory";
def chooseColor(state : Command) : Color = {
if (state == null)
Color.red
else
state.phase match {
case Phase.UNPROCESSED => new Color(255, 255, 192)
case Phase.FINISHED => new Color(192, 255, 192)
case Phase.FAILED => new Color(255, 192, 192)
case _ => Color.red
}
}
def withView(view : TextArea, f : (TheoryView) => Unit) {
if (view != null && view.getBuffer() != null)
view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match {
case null => null
case view: TheoryView => f(view)
case _ => null
}
}
def activateTextArea(textArea : TextArea) {
withView(textArea, _.activate(textArea))
}
def deactivateTextArea(textArea : TextArea) {
withView(textArea, _.deactivate(textArea))
}
}
class TheoryView(prover : Prover, buffer : JEditBuffer)
extends TextAreaExtension with Text with BufferListener {
import TheoryView._
import Text.Changed
var textArea : TextArea = null;
var col : Changed = null;
val colTimer = new Timer(300, new ActionListener() {
override def actionPerformed(e : ActionEvent) { commit() }
})
val changesSource = new EventSource[Changed]
{
buffer.addBufferListener(this)
buffer.setProperty(ISABELLE_THEORY_PROPERTY, this)
prover.commandInfo.add(e => repaint(e.command))
prover.commandInfo.add(e => repaintAll())
Plugin.plugin.viewFontChanged.add(font => updateFont())
colTimer.stop
colTimer.setRepeats(true)
}
def activate(area : TextArea) {
textArea = area
textArea.addCaretListener(selectedStateController)
val painter = textArea.getPainter()
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
updateFont()
}
private def updateFont() {
if (textArea != null) {
val painter = textArea.getPainter()
if (Plugin.plugin.viewFont != null) {
painter.setStyles(painter.getStyles().map(style =>
new SyntaxStyle(style.getForegroundColor,
style.getBackgroundColor,
Plugin.plugin.viewFont)
))
painter.setFont(Plugin.plugin.viewFont)
repaintAll()
}
}
}
def deactivate(area : TextArea) {
textArea.getPainter().removeExtension(this)
textArea.removeCaretListener(selectedStateController)
textArea = null
}
val selectedStateController = new CaretListener() {
override def caretUpdate(e : CaretEvent) {
val cmd = prover.document.getNextCommandContaining(e.getDot())
if (cmd != null && cmd.start <= e.getDot() &&
Plugin.plugin.selectedState != cmd)
Plugin.plugin.selectedState = cmd
}
}
private def fromCurrent(pos : Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.added) col.start
else pos - col.added + col.removed
else pos
private def toCurrent(pos : Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.removed) col.start
else pos + col.added - col.removed
else pos
def repaint(cmd : Command)
{
var ph = cmd.phase
if (textArea != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
var start = textArea.getLineOfOffset(toCurrent(cmd.start))
var stop = textArea.getLineOfOffset(toCurrent(cmd.stop) - 1)
textArea.invalidateLineRange(start, stop)
if (Plugin.plugin.selectedState == cmd)
Plugin.plugin.selectedState = cmd // update State view
}
}
def repaintAll()
{
if (textArea != null)
textArea.invalidateLineRange(textArea.getFirstPhysicalLine,
textArea.getLastPhysicalLine)
}
override def paintValidLine(gfx : Graphics2D, screenLine : Int,
pl : Int, start : Int, end : Int, y : Int)
{
var fm = textArea.getPainter().getFontMetrics()
var savedColor = gfx.getColor()
var e = prover.document.getNextCommandContaining(fromCurrent(start))
while (e != null && toCurrent(e.start) < end) {
val begin = Math.max(start, toCurrent(e.start))
val startP = textArea.offsetToXY(begin)
val finish = Math.min(end - 1, toCurrent(e.stop))
val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish)
else { var p = textArea.offsetToXY(finish - 1)
p.x = p.x + fm.charWidth(' ')
p }
if (startP != null && stopP != null) {
gfx.setColor(chooseColor(e))
gfx.fillRect(startP.x, y, stopP.x - startP.x, fm.getHeight())
}
e = e.next
}
gfx.setColor(savedColor)
}
def content(start : Int, stop : Int) = buffer.getText(start, stop - start)
def length = buffer.getLength()
def changes = changesSource
private def commit() {
if (col != null)
changes.fire(col)
col = null
if (colTimer.isRunning())
colTimer.stop()
}
private def delayCommit() {
if (colTimer.isRunning())
colTimer.restart()
else
colTimer.start()
}
override def contentInserted(buffer : JEditBuffer, startLine : Int,
offset : Int, numLines : Int, length : Int) {
if(length > 1) {
//longer text inserted -> convert it
val text = buffer.getText(offset, length)
val decoded = VFS.converter.decode(text)
if(!text.equals(decoded)){
buffer.remove(offset, length)
buffer.insert(offset, decoded)
}
}
}
override def contentRemoved(buffer : JEditBuffer, startLine : Int,
offset : Int, numLines : Int, length : Int) { }
override def preContentInserted(buffer : JEditBuffer, startLine : Int,
offset : Int, numLines : Int, length : Int) {
//simple xsymbol detection: entering whitespace after '>' checks for xsymbol
if(length == 1 && offset - 1 > 0 && buffer.getText(offset - 1, 2).equals("> ")){
val MAX_XSYMB_LENGTH = 20
var beginning = offset - 2
var length = 2
while(length < MAX_XSYMB_LENGTH && beginning > 0 && !buffer.getText(beginning, 1).equals("\\")){
beginning -= 1
length += 1
}
if(beginning >= 0 && buffer.getText(beginning, 2).equals("\\<")){
val candidate = buffer.getText(beginning, length)
val decoded = VFS.converter.decode(candidate)
buffer.remove(beginning, length)
buffer.insert(beginning, decoded)
}
}
if (col == null)
col = new Changed(offset, length, 0)
else if (col.start <= offset && offset <= col.start + col.added)
col = new Changed(col.start, col.added + length, col.removed)
else {
commit()
col = new Changed(offset, length, 0)
}
delayCommit()
}
override def preContentRemoved(buffer : JEditBuffer, startLine : Int,
start : Int, numLines : Int, removed : Int) {
if (col == null)
col = new Changed(start, 0, removed)
else if (col.start > start + removed || start > col.start + col.added) {
commit()
col = new Changed(start, 0, removed)
}
else {
val offset = start - col.start
val diff = col.added - removed
val (added, addRemoved) =
if (diff < offset)
(offset max 0, diff - (offset max 0))
else
(diff - (offset min 0), offset min 0)
col = new Changed(start min col.start, added, col.removed - addRemoved)
}
delayCommit()
}
override def bufferLoaded(buffer : JEditBuffer) { }
override def foldHandlerChanged(buffer : JEditBuffer) { }
override def foldLevelChanged(buffer : JEditBuffer, startLine : Int,
endLine : Int) = { }
override def transactionComplete(buffer : JEditBuffer) = { }
}