# HG changeset patch
# User wenzelm
# Date 1262193730 -3600
# Node ID 0b788ea1ceac68a4418caa8bf6a6649da1d62ee0
# Parent  f0107bc96961696c30cbc07ff7132793fb314fd3
removed experimental history panel;

diff -r f0107bc96961 -r 0b788ea1ceac src/Tools/jEdit/dist-template/properties/jedit.props
--- 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
diff -r f0107bc96961 -r 0b788ea1ceac src/Tools/jEdit/plugin/Isabelle.props
--- 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
diff -r f0107bc96961 -r 0b788ea1ceac src/Tools/jEdit/plugin/actions.xml
--- 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
diff -r f0107bc96961 -r 0b788ea1ceac src/Tools/jEdit/plugin/dockables.xml
--- 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
diff -r f0107bc96961 -r 0b788ea1ceac src/Tools/jEdit/src/jedit/document_model.scala
--- 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] =
diff -r f0107bc96961 -r 0b788ea1ceac src/Tools/jEdit/src/jedit/history_dockable.scala
--- 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())
-}