--- 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)
+ }
+ }
+ }
+
}