some support to prune_history;
clarified signature: recent_stable is supposed to be always defined;

--- a/src/Pure/PIDE/document.scala	Fri Sep 02 16:58:00 2011 -0700
+++ b/src/Pure/PIDE/document.scala	Sat Sep 03 12:31:27 2011 +0200
@@ -168,15 +168,19 @@
 
   object Change
   {
-    val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init))
+    val init: Change = Change(Some(Future.value(Version.init)), Nil, Future.value(Version.init))
   }
 
   sealed case class Change(
-    val previous: Future[Version],
+    val previous: Option[Future[Version]],
     val edits: List[Edit_Text],
     val version: Future[Version])
   {
-    def is_finished: Boolean = previous.is_finished && version.is_finished
+    def is_finished: Boolean =
+      (previous match { case None => true case Some(future) => future.is_finished }) &&
+      version.is_finished
+
+    def truncate: Change = copy(previous = None, edits = Nil)
   }
 
 
@@ -184,16 +188,16 @@
 
   object History
   {
-    val init: History = new History(List(Change.init))
+    val init: History = History(List(Change.init))
   }
 
   // FIXME pruning, purging of state
-  class History(val undo_list: List[Change])
+  sealed case class History(val undo_list: List[Change])
   {
     require(!undo_list.isEmpty)
 
     def tip: Change = undo_list.head
-    def +(change: Change): History = new History(change :: undo_list)
+    def +(change: Change): History = copy(undo_list = change :: undo_list)
   }
 
 
@@ -342,7 +346,7 @@
     def is_stable(change: Change): Boolean =
       change.is_finished && is_assigned(change.version.get_finished)
 
-    def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+    def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
     def tip_stable: Boolean = is_stable(history.tip)
     def tip_version: Version = history.tip.version.get_finished
 
@@ -366,10 +370,25 @@
         edits: List[Edit_Text],
         version: Future[Version]): (Change, State) =
     {
-      val change = Change(previous, edits, version)
+      val change = Change(Some(previous), edits, version)
       (change, copy(history = history + change))
     }
 
+    def prune_history(retain: Int = 0): (List[Version], State) =
+    {
+      val undo_list = history.undo_list
+      val n = undo_list.iterator.zipWithIndex.find(p => is_stable(p._1)).get._2 + 1
+      val (retained, dropped) = undo_list.splitAt(n max retain)
+
+      retained.splitAt(retained.length - 1) match {
+        case (prefix, List(last)) =>
+          val dropped_versions = dropped.map(change => change.version.get_finished)
+          val state1 = copy(history = History(prefix ::: List(last.truncate)))
+          (dropped_versions, state1)
+        case _ => fail
+      }
+    }
+
     def command_state(version: Version, command: Command): Command.State =
     {
       require(is_assigned(version))
@@ -384,7 +403,7 @@
     // persistent user-view
     def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
     {
-      val stable = recent_stable.get
+      val stable = recent_stable
       val latest = history.tip
 
       // FIXME proper treatment of removed nodes

--- a/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 02 16:58:00 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 03 12:31:27 2011 +0200
@@ -80,23 +80,21 @@
     Swing_Thread.now {
       // FIXME correlation to changed_nodes!?
       val state = Isabelle.session.current_state()
-      state.recent_stable.map(change => change.version.get_finished) match {
-        case None =>
-        case Some(version) =>
-          var nodes_status1 = nodes_status
-          for {
-            name <- changed_nodes
-            node <- version.nodes.get(name)
-            val status = Isar_Document.node_status(state, version, node)
-          } nodes_status1 += (name -> status.toString)
+      val version = state.recent_stable.version.get_finished
 
-          if (nodes_status != nodes_status1) {
-            nodes_status = nodes_status1
-            val order =
-              Library.sort_wrt((name: Document.Node.Name) => name.theory,
-                nodes_status.keySet.toList)
-            status.listData = order.map(name => name.theory + " " + nodes_status(name))
-          }
+      var nodes_status1 = nodes_status
+      for {
+        name <- changed_nodes
+        node <- version.nodes.get(name)
+        val status = Isar_Document.node_status(state, version, node)
+      } nodes_status1 += (name -> status.toString)
+
+      if (nodes_status != nodes_status1) {
+        nodes_status = nodes_status1
+        val order =
+          Library.sort_wrt((name: Document.Node.Name) => name.theory,
+            nodes_status.keySet.toList)
+        status.listData = order.map(name => name.theory + " " + nodes_status(name))
       }
     }
   }