eliminated redundant session documents database;
tuned;

--- a/src/Tools/jEdit/src/proofdocument/document.scala	Fri Jan 01 21:37:37 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Fri Jan 01 21:45:26 2010 +0100
@@ -60,7 +60,7 @@
     val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
     val token_start: Map[Token, Int],  // FIXME eliminate
     val commands: Linear_Set[Command],
-    var states: Map[Command, Command])   // FIXME immutable, eliminate!?
+    @volatile var states: Map[Command, Command])   // FIXME immutable, eliminate!?
   extends Session.Entity
 {
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Fri Jan 01 21:37:37 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Fri Jan 01 21:45:26 2010 +0100
@@ -48,7 +48,8 @@
   def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
 
 
-  /* document state information -- owned by session_actor */
+
+  /** main actor **/
 
   @volatile private var syntax = new Outer_Syntax(system.symbols)
   def current_syntax: Outer_Syntax = syntax
@@ -56,14 +57,6 @@
   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
   def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
 
-  // FIXME eliminate
-  @volatile private var documents = Map[Isar_Document.Document_ID, Document]()
-  def document(id: Isar_Document.Document_ID): Option[Document] = documents.get(id)
-
-
-
-  /** main actor **/
-
   private case class Register(entity: Session.Entity)
   private case class Start(timeout: Int, args: List[String])
   private case object Stop
@@ -95,7 +88,6 @@
             })
       }
       register(doc)
-      documents += (doc.id -> doc)  // FIXME remove
       prover.edit_document(change.parent.get.document.id, doc.id, id_changes)
 
       document_change.event(doc)
@@ -202,7 +194,6 @@
           val id = create_id()
           val doc = Document.empty(id)
           register(doc)
-          documents += (id -> doc)
           prover.begin_document(id, path)
           reply(doc)
 
@@ -221,7 +212,6 @@
 
   /* main methods */
 
-  // FIXME private?
   def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
 
   def start(timeout: Int, args: List[String]): Option[String] =