--- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed Dec 30 17:48:58 2009 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed Dec 30 18:22:10 2009 +0100
@@ -170,7 +170,6 @@
encodingDetectors=BOM XML-PI buffer-local-property
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
-isabelle-history.dock-position=bottom
isabelle-protocol.dock-position=bottom
isabelle-results.dock-position=bottom
isabelle.activate.shortcut=CS+ENTER
--- a/src/Tools/jEdit/plugin/Isabelle.props Wed Dec 30 17:48:58 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Wed Dec 30 18:22:10 2009 +0100
@@ -29,16 +29,14 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol isabelle.show-history
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol
isabelle.activate.label=Activate current buffer
isabelle.show-output.label=Show Output
isabelle.show-protocol.label=Show Protocol
-isabelle.show-history.label=Show History
#dockables
isabelle-output.title=Output
isabelle-protocol.title=Protocol
-isabelle-history.title=History
#SideKick
sidekick.parser.isabelle.label=Isabelle
--- a/src/Tools/jEdit/plugin/actions.xml Wed Dec 30 17:48:58 2009 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml Wed Dec 30 18:22:10 2009 +0100
@@ -20,9 +20,4 @@
wm.addDockableWindow("isabelle-protocol");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.show-history">
- <CODE>
- wm.addDockableWindow("isabelle-history");
- </CODE>
- </ACTION>
</ACTIONS>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/dockables.xml Wed Dec 30 17:48:58 2009 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml Wed Dec 30 18:22:10 2009 +0100
@@ -8,7 +8,4 @@
<DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
new isabelle.jedit.Protocol_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-history" MOVABLE="TRUE">
- new isabelle.jedit.History_Dockable(view, position).peer ();
- </DOCKABLE>
</DOCKABLES>
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Dec 30 17:48:58 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Dec 30 18:22:10 2009 +0100
@@ -106,59 +106,6 @@
def current_document() = doc_or_pred(current_change)
- /* update to desired version */
-
- def set_version(goal: Change)
- {
- // changes in buffer must be ignored
- buffer.removeBufferListener(buffer_listener)
-
- def apply(change: Change): Unit =
- change.edits.foreach {
- case Insert(start, text) => buffer.insert(start, text)
- case Remove(start, text) => buffer.remove(start, text.length)
- }
-
- def unapply(change: Change): Unit =
- change.edits.reverse.foreach {
- case Insert(start, text) => buffer.remove(start, text.length)
- case Remove(start, text) => buffer.insert(start, text)
- }
-
- // 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
- buffer.propertiesChanged()
- // invalidate_all() FIXME
- // overview.repaint() FIXME
-
- // track changes in buffer
- buffer.addBufferListener(buffer_listener)
- }
-
-
/* transforming offsets */
private def changes_from(doc: Proof_Document): List[Edit] =
--- a/src/Tools/jEdit/src/jedit/history_dockable.scala Wed Dec 30 17:48:58 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-/*
- * Dockable window for navigating through the document history
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-
-import isabelle.proofdocument.Change
-
-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 History_Dockable(view: View, position: String) extends FlowPanel
-{
- if (position == DockableWindowManager.FLOATING)
- preferredSize = new Dimension(500, 250)
-
- def get_versions() =
- Document_Model(view.getBuffer) match {
- case None => Nil
- case Some(model) => model.changes
- }
-
- val list = new ListView[Change]
- list.fixedCellWidth = 500
- list.listData = get_versions()
- contents += list
-
- listenTo(list.selection)
- reactions += {
- case ListSelectionChanged(source, range, false) =>
- Document_Model(view.getBuffer).map(_.set_version(list.listData(range.start)))
- }
-
- if (Document_Model(view.getBuffer).isDefined)
- Isabelle.session.document_change += (_ => list.listData = get_versions())
-}