# HG changeset patch # User immler@in.tum.de # Date 1251363069 -7200 # Node ID 1f1f6c95de643817f7de8e17013611d4a6436b7a # Parent 8be4cdbbe3a7075481875b565cb2e7906943e1d8 clarified structure of TheoryView diff -r 8be4cdbbe3a7 -r 1f1f6c95de64 src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala --- a/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Thu Aug 27 10:51:09 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Thu Aug 27 10:51:09 2009 +0200 @@ -27,7 +27,7 @@ new javax.swing.Timer(1000, new java.awt.event.ActionListener { override def actionPerformed(evt: java.awt.event.ActionEvent) { list.listData = Isabelle.prover_setup(view.getBuffer).map(_. - theory_view.get_changes).getOrElse(Nil) + theory_view.changes).getOrElse(Nil) } }).start() diff -r 8be4cdbbe3a7 -r 1f1f6c95de64 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200 @@ -42,30 +42,18 @@ class TheoryView (text_area: JEditTextArea) extends TextAreaExtension with BufferListener { - - def id() = Isabelle.system.id() - private val buffer = text_area.getBuffer + val buffer = text_area.getBuffer // start prover val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic, change_receiver) prover.start() // start actor - private var edits: List[Edit] = Nil - private val col_timer = new Timer(300, new ActionListener() { - override def actionPerformed(e: ActionEvent) = commit - }) - - col_timer.stop - col_timer.setRepeats(true) - + /* activation */ private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current) - - /* activation */ - private val selected_state_controller = new CaretListener { override def caretUpdate(e: CaretEvent) = { val doc = current_document() @@ -103,126 +91,12 @@ } - /* painting */ - - val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() } - - private def lines_of_command(cmd: Command) = - { - val document = current_document() - (text_area.getLineOfOffset(to_current(document, cmd.start(document))), - text_area.getLineOfOffset(to_current(document, cmd.stop(document)))) - } - - 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() - } - - lazy val change_receiver = actor { - loop { - react { - case ProverEvents.Activate => - edits = List(Insert(0, buffer.getText(0, buffer.getLength))) - commit - case c: Command => - Swing_Thread.later { - update_syntax(c) - invalidate_line(c) - phase_overview.repaint() - } - case x => System.err.println("warning: change_receiver ignored " + x) - } - } - } - - - def changes_to(doc: ProofDocument) = - edits ::: current_change.ancestors(_.id == doc.id).flatten(_.toList) - - def from_current(doc: ProofDocument, pos: Int) = - (pos /: changes_to(doc)) ((p, c) => c from_where p) - - def to_current(doc: ProofDocument, pos: Int) = - (pos /: changes_to(doc).reverse) ((p, c) => c where_to p) - - def invalidate_line(cmd: Command) = - { - val (start, stop) = lines_of_command(cmd) - text_area.invalidateLineRange(start, stop) - - if (Isabelle.plugin.selected_state == cmd) - Isabelle.plugin.selected_state = cmd // update State view - } - - def invalidate_all() = - text_area.invalidateLineRange(text_area.getFirstPhysicalLine, - text_area.getLastPhysicalLine) - - 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) - } - } - - - /* 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 e = document.find_command_at(from_current(start)) - while (e != null && e.start(document) < end) { - 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) - e = document.commands.next(e).getOrElse(null) - } - - gfx.setColor(saved_color) - } - - override def getToolTipText(x: Int, y: Int) = { - val document = current_document() - val offset = from_current(document, text_area.xyToOffset(x, y)) - val cmd = document.find_command_at(offset) - if (cmd != null) { - document.token_start(cmd.tokens.first) - cmd.type_at(document, offset - cmd.start(document)) - } else null - } - /* history of changes - TODO: seperate class?*/ - val change_0: Change = new Change(prover.document_0.id, None, Nil) - private var changes = List(change_0) + private val change_0 = new Change(prover.document_0.id, None, Nil) + private var _changes = List(change_0) + def changes = _changes private var current_change = change_0 - def get_changes = changes private def doc_or_pred(c: Change): ProofDocument = prover.document(c.id).getOrElse(doc_or_pred(c.parent.get)) @@ -277,12 +151,21 @@ buffer.addBufferListener(this) } - /* BufferListener methods */ + /* sending edits to prover */ + + private var edits: List[Edit] = Nil + + private val col_timer = new Timer(300, new ActionListener() { + override def actionPerformed(e: ActionEvent) = commit + }) + + col_timer.stop + col_timer.setRepeats(true) private def commit: Unit = synchronized { if (!edits.isEmpty) { val change = new Change(Isabelle.system.id(), Some(current_change), edits) - changes ::= change + _changes ::= change prover ! change current_change = change } @@ -298,6 +181,7 @@ col_timer.start() } + /* BufferListener methods */ override def contentInserted(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, length: Int) { } @@ -324,4 +208,124 @@ override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } override def transactionComplete(buffer: JEditBuffer) { } + + /* transforming offsets */ + + private def changes_to(doc: ProofDocument) = + edits ::: current_change.ancestors(_.id == doc.id).flatten(_.toList) + + def from_current(doc: ProofDocument, pos: Int) = + (pos /: changes_to(doc)) ((p, c) => c from_where p) + + def to_current(doc: ProofDocument, pos: Int) = + (pos /: changes_to(doc).reverse) ((p, c) => c where_to p) + + + private def lines_of_command(cmd: Command) = + { + val document = current_document() + (text_area.getLineOfOffset(to_current(document, cmd.start(document))), + text_area.getLineOfOffset(to_current(document, cmd.stop(document)) - 1)) + } + + + /* (re)painting */ + + private val update_delay = Swing_Thread.delay(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.plugin.selected_state == cmd) + Isabelle.plugin.selected_state = cmd // update State view + } + + 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) + } + } + + /* 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 e = document.find_command_at(from_current(start)) + while (e != null && e.start(document) < end) { + 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) + e = document.commands.next(e).getOrElse(null) + } + + gfx.setColor(saved_color) + } + + override def getToolTipText(x: Int, y: Int) = { + val document = current_document() + val offset = from_current(document, text_area.xyToOffset(x, y)) + val cmd = document.find_command_at(offset) + if (cmd != null) { + document.token_start(cmd.tokens.first) + cmd.type_at(document, offset - cmd.start(document)) + } else null + } + + + /* receiving from prover */ + + lazy val change_receiver: Actor = actor { + loop { + react { + case ProverEvents.Activate => + edits = List(Insert(0, buffer.getText(0, buffer.getLength))) + commit + case c: Command => + Swing_Thread.later { + update_syntax(c) + invalidate_line(c) + phase_overview.repaint() + } + case x => System.err.println("warning: change_receiver ignored " + x) + } + } + } + }