--- a/src/Tools/jEdit/src/proofdocument/session.scala Fri Jan 01 22:29:08 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Sun Jan 03 19:53:58 2010 +0100
@@ -39,7 +39,6 @@
val results = new Event_Bus[Command]
val command_change = new Event_Bus[Command]
- val document_change = new Event_Bus[Document]
/* unique ids */
@@ -81,7 +80,7 @@
(c1.map(_.id).getOrElse(""),
c2 match {
case None => None
- case Some(command) => // FIXME clarify -- may reuse existing commands!??
+ case Some(command) => // FIXME register/define only commands unknown to prover
register(command)
prover.define_command(command.id, system.symbols.encode(command.content))
Some(command.id)
@@ -89,8 +88,6 @@
}
register(doc)
prover.edit_document(change.parent.get.document.id, doc.id, id_changes)
-
- document_change.event(doc)
}