# HG changeset patch # User immler@in.tum.de # Date 1247488239 -7200 # Node ID 30f588245884f5207a8e3e7d2128825f801394a6 # Parent 2e033aaf128ef130bf19cbfc332d8c39804a5f9c arbitrary history diff -r 2e033aaf128e -r 30f588245884 src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala --- a/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Wed Jul 08 15:15:15 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Mon Jul 13 14:30:39 2009 +0200 @@ -18,7 +18,6 @@ class BrowseVersionDockable(view : View, position : String) extends FlowPanel { - val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view if (position == DockableWindowManager.FLOATING) preferredSize = new Dimension(500, 250) @@ -27,7 +26,8 @@ new javax.swing.Timer(1000, new java.awt.event.ActionListener { override def actionPerformed(evt: java.awt.event.ActionEvent) { - list.listData_=(theory_view.get_changes) + list.listData = Isabelle.prover_setup(view.getBuffer).map(_. + theory_view.get_changes).getOrElse(Nil) } }).start() @@ -37,7 +37,8 @@ reactions += { case ListSelectionChanged(source, range, false) => Swing_Thread.now { - theory_view.set_version(list.listData(range.start).id) + Isabelle.prover_setup(view.getBuffer).map(_. + theory_view.set_version(list.listData(range.start))) } } } diff -r 2e033aaf128e -r 30f588245884 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 15:15:15 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Jul 13 14:30:39 2009 +0200 @@ -108,8 +108,8 @@ val theory_view = Isabelle.prover_setup(buffer).get.theory_view val document = theory_view.current_document() - def to: Int => Int = theory_view.to_current(document.id, _) - def from: Int => Int = theory_view.from_current(document.id, _) + def to: Int => Int = theory_view.to_current(document, _) + def from: Int => Int = theory_view.from_current(document, _) var command = document.find_command_at(from(start)) var next_x = start diff -r 2e033aaf128e -r 30f588245884 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Jul 08 15:15:15 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Jul 13 14:30:39 2009 +0200 @@ -6,7 +6,7 @@ package isabelle.jedit -import isabelle.prover.Command +import isabelle.prover.{Prover, Command} import isabelle.proofdocument.ProofDocument import javax.swing._ @@ -17,9 +17,12 @@ import org.gjt.sp.jedit.buffer.JEditBuffer; import org.gjt.sp.jedit._ -class PhaseOverviewPanel(prover: isabelle.prover.Prover, - textarea: JEditTextArea, - to_current: (String, Int) => Int) extends JPanel(new BorderLayout) { +class PhaseOverviewPanel( + prover: Prover, + textarea: JEditTextArea, + to_current: (ProofDocument, Int) => Int) +extends JPanel(new BorderLayout) +{ private val WIDTH = 10 private val HILITE_HEIGHT = 2 @@ -59,8 +62,8 @@ } private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) { - val line1 = buffer.getLineOfOffset(to_current(doc.id, command.start(doc))) - val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc))) + 1 + val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc))) + val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1 val y = lineToY(line1) val height = lineToY(line2) - y - 1 val (light, dark) = command.status(doc) match { diff -r 2e033aaf128e -r 30f588245884 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 15:15:15 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Jul 13 14:30:39 2009 +0200 @@ -52,9 +52,6 @@ private var col: Text.Change = null - private var doc_id: IsarDocument.Document_ID = prover.document(null).id - def current_document() = prover.document(doc_id) - private val col_timer = new Timer(300, new ActionListener() { override def actionPerformed(e: ActionEvent) = commit }) @@ -85,7 +82,7 @@ buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) buffer.addBufferListener(this) - col = Text.Change(doc_id, Isabelle.system.id(), 0, + col = Text.Change(Some(current_change), Isabelle.system.id(), 0, buffer.getText(0, buffer.getLength), "") commit } @@ -118,76 +115,45 @@ } } - def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int = - changes match { - case Nil => pos - case Text.Change(_, id, start, added, removed) :: rest_changes => { - val shifted = - if (start <= pos) - if (pos < start + added.length) start - else pos - added.length + removed.length - else pos - if (id == to_id) pos - else _from_current(to_id, rest_changes, shifted) - } - } - def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int = - changes match { - case Nil => pos - case Text.Change(_, id, start, added, removed) :: rest_changes => { - val shifted = _to_current(from_id, rest_changes, pos) - if (id == from_id) pos - else if (start <= shifted) { - if (shifted < start + removed.length) start - else shifted + added.length - removed.length - } else shifted - } + def transform_back(from: Text.Change, to: Text.Change, pos: Int): Int = + if (from.id == to.id) pos + else { + val shifted = + if (from.start <= pos) + if (pos < from.start + from.added.length) from.start + else pos - from.added.length + from.removed.length + else pos + transform_back(from.base.get, to, shifted) } - def to_current(from_id: String, pos: Int) = _to_current(from_id, - if (col == null) current_changes else col :: current_changes, pos) - def from_current(to_id: String, pos: Int) = _from_current(to_id, - if (col == null) current_changes else col :: current_changes, pos) - def to_current(doc: isabelle.proofdocument.ProofDocument, pos: Int): Int = - to_current(doc.id, pos) - def from_current(doc: isabelle.proofdocument.ProofDocument, pos: Int): Int = - from_current(doc.id, pos) - - /* update to desired version */ - - def set_version(id: String) { - // changes in buffer must be ignored - buffer.removeBufferListener(this) - - val base = changes.find(_.id == doc_id).get - val goal = changes.find(_.id == id).get - - if (changes.indexOf(base) < changes.indexOf(goal)) - changes.dropWhile(_ != base).takeWhile(_ != goal).map { c => - buffer.remove(c.start, c.added.length) - buffer.insert(c.start, c.removed)} - else - changes.dropWhile(_ != goal).takeWhile(_ != base).reverse.map { c => - buffer.remove(c.start, c.removed.length) - buffer.insert(c.start, c.added)} - - val content = buffer.getText(0, buffer.getLength) - doc_id = id - // invoke repaint - update_delay() - repaint_delay() - phase_overview.repaint_delay() - - buffer.addBufferListener(this) + def transform_forward(from: Text.Change, to: Text.Change, pos: Int): Int = + if (from.id == to.id) pos + else { + val shifted = transform_forward(from, to.base.get, pos) + if (to.start <= shifted) { + if (shifted < to.start + to.removed.length) to.start + else shifted + to.added.length - to.removed.length + } else shifted + } + + def from_current(doc: ProofDocument, pos: Int) = { + val from = if (col == null) current_change else col + val to = changes.find(_.id == doc.id).get + transform_back(from, to, pos) + } + def to_current(doc: ProofDocument, pos: Int) = { + val from = changes.find(_.id == doc.id).get + val to = if (col == null) current_change else col + transform_forward(from, to, pos) } def repaint(cmd: Command) = { val document = current_document() if (text_area != null) { - val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document))) - val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1) + val start = text_area.getLineOfOffset(to_current(document, cmd.start(document))) + val stop = text_area.getLineOfOffset(to_current(document, cmd.stop(document)) - 1) text_area.invalidateLineRange(start, stop) if (Isabelle.prover_setup(buffer).get.selected_state == cmd) @@ -228,8 +194,8 @@ 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.id, pos) - def to_current(pos: Int) = this.to_current(document.id, pos) + 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 @@ -249,7 +215,7 @@ override def getToolTipText(x: Int, y: Int) = { val document = current_document() - val offset = from_current(document.id, text_area.xyToOffset(x, y)) + 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) @@ -257,25 +223,77 @@ } else null } - /* BufferListener methods */ + /* history of changes - TODO: seperate class?*/ + + val change_0 = Text.Change(None, prover.document_0.id, 0, "", "") + private var changes = List(change_0) + private var current_change = change_0 + def get_changes = changes + + private def doc_or_pred(c: Text.Change): ProofDocument = + prover.document(c.id).getOrElse(doc_or_pred(c.base.get)) + def current_document() = doc_or_pred(current_change) + + /* update to desired version */ + + def set_version(goal: Text.Change) { + // changes in buffer must be ignored + buffer.removeBufferListener(this) + + def apply(c: Text.Change) = { + buffer.remove(c.start, c.removed.length) + buffer.insert(c.start, c.added)} + def unapply(c: Text.Change) = { + buffer.remove(c.start, c.added.length) + buffer.insert(c.start, c.removed)} - private var changes: List[Text.Change] = Nil - private def current_changes = changes.dropWhile(_.id != doc_id) - def get_changes = changes + // 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 + update_delay() + repaint_delay() + phase_overview.repaint_delay() + + //track changes in buffer + buffer.addBufferListener(this) + } + + /* BufferListener methods */ private def commit: Unit = synchronized { if (col != null) { def split_changes(c: Text.Change): List[Text.Change] = { val MAX = TheoryView.MAX_CHANGE_LENGTH if (c.added.length <= MAX) List(c) - else Text.Change(c.base_id, c.id, c.start, c.added.substring(0, MAX), c.removed) :: - split_changes(new Text.Change(c.id, id(), c.start + MAX, c.added.substring(MAX), "")) + else Text.Change(c.base, c.id, c.start, c.added.substring(0, MAX), c.removed) :: + split_changes(Text.Change(Some(c), id(), c.start + MAX, c.added.substring(MAX), "")) } val new_changes = split_changes(col) - changes = new_changes.reverse ::: current_changes - doc_id = new_changes.head.id + changes ++= new_changes new_changes map (document_actor ! _) - doc_id = new_changes.last.id + current_change = new_changes.last } col = null if (col_timer.isRunning()) @@ -301,12 +319,13 @@ { val text = buffer.getText(offset, length) if (col == null) - col = new Text.Change(doc_id, id(), offset, text, "") + col = new Text.Change(Some(current_change), id(), offset, text, "") else if (col.start <= offset && offset <= col.start + col.added.length) - col = new Text.Change(doc_id, col.id, col.start, col.added + text, col.removed) + col = new Text.Change(Some(current_change), col.id, + col.start, col.added + text, col.removed) else { commit - col = new Text.Change(doc_id, id(), offset, text, "") + col = new Text.Change(Some(current_change), id(), offset, text, "") } delay_commit } @@ -316,10 +335,10 @@ { val removed = buffer.getText(start, removed_length) if (col == null) - col = new Text.Change(doc_id, id(), start, "", removed) + col = new Text.Change(Some(current_change), id(), start, "", removed) else if (col.start > start + removed_length || start > col.start + col.added.length) { commit - col = new Text.Change(doc_id, id(), start, "", removed) + col = new Text.Change(Some(current_change), id(), start, "", removed) } else { /* val offset = start - col.start @@ -331,7 +350,7 @@ (diff - (offset min 0), offset min 0) col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/ commit - col = new Text.Change(doc_id, id(), start, "", removed) + col = new Text.Change(Some(current_change), id(), start, "", removed) } delay_commit } diff -r 2e033aaf128e -r 30f588245884 src/Tools/jEdit/src/proofdocument/Text.scala --- a/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 15:15:15 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/Text.scala Mon Jul 13 14:30:39 2009 +0200 @@ -9,11 +9,15 @@ object Text { case class Change( - base_id: String, + base: Option[Change], id: String, start: Int, added: String, - removed: String) { + removed: String) + { override def toString = id + ": added '" + added + "'; removed '" + removed + "'" + + def ancestors: List[Text.Change] = + this :: base.map(_.ancestors).getOrElse(Nil) } -} \ No newline at end of file +} diff -r 2e033aaf128e -r 30f588245884 src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 15:15:15 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Jul 13 14:30:39 2009 +0200 @@ -45,13 +45,12 @@ mutable.SynchronizedMap[IsarDocument.State_ID, Command] private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with mutable.SynchronizedMap[IsarDocument.Command_ID, Command] - private val document_0 = + val document_0 = ProofDocument.empty.set_command_keyword(command_decls.contains) private var document_versions = List(document_0) def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id) - def document(id: IsarDocument.Document_ID) = - document_versions.find(_.id == id).getOrElse(document_0) + def document(id: IsarDocument.Document_ID) = document_versions.find(_.id == id) private var initialized = false @@ -230,7 +229,7 @@ loop { react { case change: Text.Change => { - val old = document(change.base_id) + val old = document(change.base.get.id).get val (doc, structure_change) = old.text_changed(change) document_versions ::= doc edit_document(old, doc, structure_change)