--- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed Jul 08 13:29:44 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed Jul 08 15:15:13 2009 +0200
@@ -187,3 +187,5 @@
mode.isabelle.sidekick.showStatusWindow.label=true
sidekick-tree.dock-position=right
isabelle-state.dock-position=bottom
+isabelle-output.dock-position=bottom
+isabelle-browser.dock-position=bottom
--- a/src/Tools/jEdit/plugin/Isabelle.props Wed Jul 08 13:29:44 2009 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Wed Jul 08 15:15:13 2009 +0200
@@ -35,16 +35,18 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-state isabelle.show-output isabelle.show-scroller
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-state isabelle.show-output isabelle.show-scroller isabelle.show-browser
isabelle.activate.label=Activate current buffer
isabelle.show-state.label=Show State
isabelle.show-output.label=Show Output
isabelle.show-scroller.label=Show Scroller
+isabelle.show-browser.label=Show Version-Browser
#dockables
isabelle-output.title=Isabelle Output
isabelle-state.title=Isabelle State
isabelle-scroller.title=Isabelle Scroller
+isabelle-browser.title=Isabelle Browse-Version
#SideKick
sidekick.parser.isabelle.label=Isabelle
--- a/src/Tools/jEdit/plugin/actions.xml Wed Jul 08 13:29:44 2009 +0200
+++ b/src/Tools/jEdit/plugin/actions.xml Wed Jul 08 15:15:13 2009 +0200
@@ -9,12 +9,17 @@
wm.addDockableWindow("isabelle-state");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.show-scroller">
+ <ACTION NAME="isabelle.show-scroller">
<CODE>
wm.addDockableWindow("isabelle-scroller");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.activate">
+ <ACTION NAME="isabelle.show-browser">
+ <CODE>
+ wm.addDockableWindow("isabelle-browser");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.activate">
<CODE>
isabelle.jedit.Isabelle.plugin().switch_active(view);
</CODE>
--- a/src/Tools/jEdit/plugin/dockables.xml Wed Jul 08 13:29:44 2009 +0200
+++ b/src/Tools/jEdit/plugin/dockables.xml Wed Jul 08 15:15:13 2009 +0200
@@ -12,4 +12,7 @@
<DOCKABLE NAME="isabelle-scroller" MOVABLE="TRUE">
new isabelle.jedit.ScrollerDockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-browser" MOVABLE="TRUE">
+ new isabelle.jedit.BrowseVersionDockable(view, position).peer();
+ </DOCKABLE>
</DOCKABLES>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Wed Jul 08 15:15:13 2009 +0200
@@ -0,0 +1,43 @@
+/*
+ * Dockable window for navigating through the document-versions
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+import isabelle.proofdocument.Text
+
+import java.awt.Dimension
+import scala.swing.{ListView, FlowPanel}
+import scala.swing.event.ListSelectionChanged
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+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)
+
+ val list = new ListView[Text.Change]
+ list.fixedCellWidth = 500
+
+ new javax.swing.Timer(1000, new java.awt.event.ActionListener {
+ override def actionPerformed(evt: java.awt.event.ActionEvent) {
+ list.listData_=(theory_view.get_changes)
+ }
+ }).start()
+
+ contents += list
+ listenTo(list.selection)
+
+ reactions += {
+ case ListSelectionChanged(source, range, false) =>
+ Swing_Thread.now {
+ theory_view.set_version(list.listData(range.start).id)
+ }
+ }
+}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:44 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 15:15:13 2009 +0200
@@ -161,12 +161,20 @@
def set_version(id: String) {
// changes in buffer must be ignored
buffer.removeBufferListener(this)
- buffer.remove(0, buffer.getLength)
- val to_undo = changes.takeWhile(_.id != id)
- to_undo.map { c =>
- buffer.remove(c.start, c.added.length)
- buffer.insert(c.start, c.removed)
- }
+
+ 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
/* listen for changes again (TODO: can it be that Listener gets events that
happenend prior to registration??) */
@@ -251,6 +259,7 @@
private var changes: List[Text.Change] = Nil
private def current_changes = changes.dropWhile(_.id != doc_id)
+ def get_changes = changes
private def commit: Unit = synchronized {
if (col != null) {
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 13:29:44 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 15:15:13 2009 +0200
@@ -14,6 +14,6 @@
start: Int,
added: String,
removed: String) {
- override def toString = "start: " + start + " added: " + added + " removed: " + removed
+ override def toString = id + ": added '" + added + "'; removed '" + removed + "'"
}
}
\ No newline at end of file