# HG changeset patch # User wenzelm # Date 1262544838 -3600 # Node ID 4ad3298781d99a8f059efb365b4e80893197eab4 # Parent 621753b73219ad50bcc7ea74dd85f324335d82c9 removed unused document_change bus; diff -r 621753b73219 -r 4ad3298781d9 src/Tools/jEdit/src/proofdocument/session.scala --- 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) }