# HG changeset patch # User wenzelm # Date 1253031268 -7200 # Node ID c0cb6bd10eecbbab5cce63252caeb76445bfb4c7 # Parent 819862460a12f4a32bd77c09d2af29e95db1f3d9 keep BufferListener and TextAreaExtension private; misc tuning; diff -r 819862460a12 -r c0cb6bd10eec src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Sep 15 18:13:30 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Sep 15 18:14:28 2009 +0200 @@ -37,9 +37,8 @@ class TheoryView(text_area: JEditTextArea) - extends TextAreaExtension with BufferListener { - val buffer = text_area.getBuffer + private val buffer = text_area.getBuffer /* prover setup */ @@ -49,6 +48,7 @@ prover.command_change += ((command: Command) => if (current_document().commands.contains(command)) Swing_Thread.later { + // FIXME proper handling of buffer vs. text areas // repaint if buffer is active if (text_area.getBuffer == buffer) { update_syntax(command) @@ -56,7 +56,98 @@ phase_overview.repaint() } }) - + + + /* changes vs. edits */ + + private val change_0 = new Change(prover.document_0.id, None, Nil) + private var _changes = List(change_0) // owned by Swing/AWT thread + def changes = _changes + private var current_change = change_0 + + private val edits = new mutable.ListBuffer[Edit] // owned by Swing thread + + private val edits_delay = Swing_Thread.delay_last(300) { + if (!edits.isEmpty) { + val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList) + _changes ::= change + prover ! change + current_change = change + edits.clear + } + } + + + /* buffer_listener */ + + private val buffer_listener = new BufferListener { + override def preContentInserted(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, length: Int) + { + edits += Insert(offset, buffer.getText(offset, length)) + edits_delay() + } + + override def preContentRemoved(buffer: JEditBuffer, + start_line: Int, start: Int, num_lines: Int, removed_length: Int) + { + edits += Remove(start, buffer.getText(start, removed_length)) + edits_delay() + } + + override def contentInserted(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, length: Int) { } + + override def contentRemoved(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, length: Int) { } + + override def bufferLoaded(buffer: JEditBuffer) { } + override def foldHandlerChanged(buffer: JEditBuffer) { } + override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } + override def transactionComplete(buffer: JEditBuffer) { } + } + + + /* text_area_extension */ + + private val text_area_extension = new TextAreaExtension { + override def paintValidLine(gfx: Graphics2D, + screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) + { + val document = current_document() + def from_current(pos: Int) = TheoryView.this.from_current(document, pos) + def to_current(pos: Int) = TheoryView.this.to_current(document, pos) + val saved_color = gfx.getColor + + val metrics = text_area.getPainter.getFontMetrics + + // encolor phase + var cmd = document.command_at(from_current(start)) + while (cmd.isDefined && cmd.get.start(document) < end) { + val e = cmd.get + val begin = start max to_current(e.start(document)) + val finish = (end - 1) min to_current(e.stop(document)) + encolor(gfx, y, metrics.getHeight, begin, finish, + TheoryView.choose_color(e, document), true) + cmd = document.commands.next(e) + } + + gfx.setColor(saved_color) + } + + override def getToolTipText(x: Int, y: Int): String = + { + val document = current_document() + val offset = from_current(document, text_area.xyToOffset(x, y)) + document.command_at(offset) match { + case Some(cmd) => + document.token_start(cmd.tokens.first) + cmd.type_at(document, offset - cmd.start(document)).getOrElse(null) + case None => null + } + } + } + /* activation */ @@ -78,9 +169,10 @@ def activate() { text_area.addCaretListener(selected_state_controller) text_area.addLeftOfScrollBar(phase_overview) - text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this) + text_area.getPainter. + addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension) buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) - buffer.addBufferListener(this) + buffer.addBufferListener(buffer_listener) val dockable = text_area.getView.getDockableWindowManager.getDockable("isabelle-output") @@ -95,29 +187,26 @@ def deactivate() { buffer.setTokenMarker(buffer.getMode.getTokenMarker) - buffer.removeBufferListener(this) - text_area.getPainter.removeExtension(this) + buffer.removeBufferListener(buffer_listener) + text_area.getPainter.removeExtension(text_area_extension) text_area.removeLeftOfScrollBar(phase_overview) text_area.removeCaretListener(selected_state_controller) } - /* history of changes - TODO: seperate class?*/ - - private val change_0 = new Change(prover.document_0.id, None, Nil) - private var _changes = List(change_0) // owned by Swing/AWT thread - def changes = _changes - private var current_change = change_0 + /* history of changes */ private def doc_or_pred(c: Change): ProofDocument = prover.document(c.id).getOrElse(doc_or_pred(c.parent.get)) + def current_document() = doc_or_pred(current_change) + /* update to desired version */ def set_version(goal: Change) { // changes in buffer must be ignored - buffer.removeBufferListener(this) + buffer.removeBufferListener(buffer_listener) def apply(change: Change): Unit = change.edits.foreach { case Insert(start, text) => buffer.insert(start, text) @@ -159,53 +248,10 @@ phase_overview.repaint() // track changes in buffer - buffer.addBufferListener(this) - } - - - /* sending edits to prover */ - - private val edits = new mutable.ListBuffer[Edit] // owned by Swing/AWT thread - - private val edits_delay = Swing_Thread.delay_last(300) { - if (!edits.isEmpty) { - val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList) - _changes ::= change - prover ! change - current_change = change - edits.clear - } + buffer.addBufferListener(buffer_listener) } - /* BufferListener methods */ - - override def preContentInserted(buffer: JEditBuffer, - start_line: Int, offset: Int, num_lines: Int, length: Int) - { - edits += Insert(offset, buffer.getText(offset, length)) - edits_delay() - } - - override def preContentRemoved(buffer: JEditBuffer, - start_line: Int, start: Int, num_lines: Int, removed_length: Int) - { - edits += Remove(start, buffer.getText(start, removed_length)) - edits_delay() - } - - override def contentInserted(buffer: JEditBuffer, - start_line: Int, offset: Int, num_lines: Int, length: Int) { } - - override def contentRemoved(buffer: JEditBuffer, - start_line: Int, offset: Int, num_lines: Int, length: Int) { } - - override def bufferLoaded(buffer: JEditBuffer) { } - override def foldHandlerChanged(buffer: JEditBuffer) { } - override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } - override def transactionComplete(buffer: JEditBuffer) { } - - /* transforming offsets */ private def changes_from(doc: ProofDocument): List[Edit] = @@ -272,45 +318,6 @@ } - /* TextAreaExtension methods */ - - override def paintValidLine(gfx: Graphics2D, - screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) - { - val document = current_document() - def from_current(pos: Int) = this.from_current(document, pos) - def to_current(pos: Int) = this.to_current(document, pos) - val saved_color = gfx.getColor - - val metrics = text_area.getPainter.getFontMetrics - - // encolor phase - var cmd = document.command_at(from_current(start)) - while (cmd.isDefined && cmd.get.start(document) < end) { - val e = cmd.get - val begin = start max to_current(e.start(document)) - val finish = (end - 1) min to_current(e.stop(document)) - encolor(gfx, y, metrics.getHeight, begin, finish, - TheoryView.choose_color(e, document), true) - cmd = document.commands.next(e) - } - - gfx.setColor(saved_color) - } - - override def getToolTipText(x: Int, y: Int): String = - { - val document = current_document() - val offset = from_current(document, text_area.xyToOffset(x, y)) - document.command_at(offset) match { - case Some(cmd) => - document.token_start(cmd.tokens.first) - cmd.type_at(document, offset - cmd.start(document)).getOrElse(null) - case None => null - } - } - - /* init */ prover.start()