# 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)
     }