src/Tools/jEdit/src/prover/Prover.scala

--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Jul 08 15:15:15 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Jul 13 14:30:39 2009 +0200
@@ -45,13 +45,12 @@
     mutable.SynchronizedMap[IsarDocument.State_ID, Command]
   private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
     mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
-  private val document_0 =
+  val document_0 =
     ProofDocument.empty.set_command_keyword(command_decls.contains)
   private var document_versions = List(document_0)
 
   def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
-  def document(id: IsarDocument.Document_ID) =
-    document_versions.find(_.id == id).getOrElse(document_0)
+  def document(id: IsarDocument.Document_ID) = document_versions.find(_.id == id)
 
   private var initialized = false
 
@@ -230,7 +229,7 @@
     loop {
       react {
         case change: Text.Change => {
-            val old = document(change.base_id)
+            val old = document(change.base.get.id).get
             val (doc, structure_change) = old.text_changed(change)
             document_versions ::= doc
             edit_document(old, doc, structure_change)