# HG changeset patch # User immler@in.tum.de # Date 1247058913 -7200 # Node ID 5fe5e00ec430b73afc3d70595e96c706318c5df9 # Parent 23271beee68abbb71057d0f3ef5217122cc1c44f gui element to set current document version diff -r 23271beee68a -r 5fe5e00ec430 src/Tools/jEdit/dist-template/properties/jedit.props --- 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 diff -r 23271beee68a -r 5fe5e00ec430 src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 23271beee68a -r 5fe5e00ec430 src/Tools/jEdit/plugin/actions.xml --- 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"); - + wm.addDockableWindow("isabelle-scroller"); - + + + wm.addDockableWindow("isabelle-browser"); + + + isabelle.jedit.Isabelle.plugin().switch_active(view); diff -r 23271beee68a -r 5fe5e00ec430 src/Tools/jEdit/plugin/dockables.xml --- 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 @@ new isabelle.jedit.ScrollerDockable(view, position); + + new isabelle.jedit.BrowseVersionDockable(view, position).peer(); + \ No newline at end of file diff -r 23271beee68a -r 5fe5e00ec430 src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala --- /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) + } + } +} diff -r 23271beee68a -r 5fe5e00ec430 src/Tools/jEdit/src/jedit/TheoryView.scala --- 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) { diff -r 23271beee68a -r 5fe5e00ec430 src/Tools/jEdit/src/proofdocument/Text.scala --- 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