--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala Tue Dec 15 13:39:30 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,305 +0,0 @@
-/*
- * jEdit text area as document text source
- *
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker} // FIXME wrong layer
-
-import scala.actors.Actor, Actor._
-import scala.collection.mutable
-
-import java.awt.{Color, Graphics2D}
-import javax.swing.event.{CaretListener, CaretEvent}
-
-import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
-
-
-object Theory_View
-{
- def choose_color(command: Command, doc: Proof_Document): Color =
- {
- command.status(doc) match {
- case Command.Status.UNPROCESSED => new Color(255, 228, 225)
- case Command.Status.FINISHED => new Color(234, 248, 255)
- case Command.Status.FAILED => new Color(255, 106, 106)
- case _ => Color.red
- }
- }
-}
-
-
-class Theory_View(session: Session, text_area: JEditTextArea)
-{
- private val buffer = text_area.getBuffer
-
-
- /* prover setup */
-
- session.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)
- invalidate_line(command)
- overview.repaint()
- }
- })
-
-
- /* changes vs. edits */
-
- private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil) // FIXME !?
- 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(session.create_id(), Some(current_change), edits.toList)
- _changes ::= change
- session.input(change)
- current_change = change
- edits.clear
- }
- }
-
-
- /* buffer_listener */
-
- private val buffer_listener: BufferListener = new BufferAdapter {
- override def contentInserted(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()
- }
- }
-
-
- /* 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) = Theory_View.this.from_current(document, pos)
- def to_current(pos: Int) = Theory_View.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,
- Theory_View.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 */
-
- private val overview = new Document_Overview(text_area, to_current)
-
- private val selected_state_controller = new CaretListener {
- override def caretUpdate(e: CaretEvent) {
- val doc = current_document()
- doc.command_at(e.getDot) match {
- case Some(cmd)
- if (doc.token_start(cmd.tokens.first) <= e.getDot &&
- Isabelle.session.selected_state != cmd) =>
- Isabelle.session.selected_state = cmd
- case _ =>
- }
- }
- }
-
- def activate()
- {
- text_area.addCaretListener(selected_state_controller)
- text_area.addLeftOfScrollBar(overview)
- text_area.getPainter.
- addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
- buffer.setTokenMarker(new Isabelle_Token_Marker(buffer))
- buffer.addBufferListener(buffer_listener)
- buffer.propertiesChanged()
- }
-
- def deactivate()
- {
- buffer.setTokenMarker(buffer.getMode.getTokenMarker)
- buffer.removeBufferListener(buffer_listener)
- text_area.getPainter.removeExtension(text_area_extension)
- text_area.removeLeftOfScrollBar(overview)
- text_area.removeCaretListener(selected_state_controller)
- }
-
-
- /* history of changes */
-
- private def doc_or_pred(c: Change): Proof_Document =
- session.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(buffer_listener)
-
- def apply(change: Change): Unit = change.edits.foreach {
- case Insert(start, text) => buffer.insert(start, text)
- case Remove(start, text) => buffer.remove(start, text.length)
- }
-
- def unapply(change: Change): Unit = change.edits.reverse.foreach {
- case Insert(start, text) => buffer.remove(start, text.length)
- case Remove(start, text) => buffer.insert(start, text)
- }
-
- // undo/redo changes
- val ancs_current = current_change.ancestors
- val ancs_goal = goal.ancestors
- val paired = ancs_current.reverse zip ancs_goal.reverse
- def last_common[A](xs: List[(A, A)]): Option[A] = {
- xs match {
- case (x, y) :: xs =>
- if (x == y)
- xs match {
- case (a, b) :: ys =>
- if (a == b) last_common(xs)
- else Some(x)
- case _ => Some(x)
- }
- else None
- case _ => None
- }
- }
- val common_anc = last_common(paired).get
-
- ancs_current.takeWhile(_ != common_anc) map unapply
- ancs_goal.takeWhile(_ != common_anc).reverse map apply
-
- current_change = goal
- // invoke repaint
- buffer.propertiesChanged()
- invalidate_all()
- overview.repaint()
-
- // track changes in buffer
- buffer.addBufferListener(buffer_listener)
- }
-
-
- /* transforming offsets */
-
- private def changes_from(doc: Proof_Document): List[Edit] =
- List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
- edits.toList
-
- def from_current(doc: Proof_Document, offset: Int): Int =
- (offset /: changes_from(doc).reverse) ((i, change) => change before i)
-
- def to_current(doc: Proof_Document, offset: Int): Int =
- (offset /: changes_from(doc)) ((i, change) => change after i)
-
-
- private def lines_of_command(cmd: Command) =
- {
- val document = current_document()
- (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
- buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
- }
-
-
- /* (re)painting */
-
- private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
-
- private def update_syntax(cmd: Command) {
- val (line1, line2) = lines_of_command(cmd)
- if (line2 >= text_area.getFirstLine &&
- line1 <= text_area.getFirstLine + text_area.getVisibleLines)
- update_delay()
- }
-
- private def invalidate_line(cmd: Command) =
- {
- val (start, stop) = lines_of_command(cmd)
- text_area.invalidateLineRange(start, stop)
-
- if (Isabelle.session.selected_state == cmd)
- Isabelle.session.selected_state = cmd
- }
-
- private def invalidate_all() =
- text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
- text_area.getLastPhysicalLine)
-
- private def encolor(gfx: Graphics2D,
- y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
- {
- val start = text_area.offsetToXY(begin)
- val stop =
- if (finish < buffer.getLength) text_area.offsetToXY(finish)
- else {
- val p = text_area.offsetToXY(finish - 1)
- val metrics = text_area.getPainter.getFontMetrics
- p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
- p
- }
-
- if (start != null && stop != null) {
- gfx.setColor(color)
- if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
- else gfx.drawRect(start.x, y, stop.x - start.x, height)
- }
- }
-
-
- /* init */
-
- edits += Insert(0, buffer.getText(0, buffer.getLength))
- edits_delay()
-}