--- 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] =