eliminated global Session.document_0 -- did not work due to hardwired id;
more precise Session.begin_document, avoid race on var prover;
replaced slightly odd Session.document_versions by Sassion.documents table (cf. src/Pure/Isar/isar_document.ML);
simplified edit_document in ML: initial empty command is identified by "";
misc tuning;

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Dec 29 15:33:39 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Dec 29 20:40:08 2009 +0100
@@ -58,8 +58,10 @@
 {
   /* changes vs. edits */
 
-  private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil)  // FIXME !?
-  private var _changes = List(change_0)   // owned by Swing/AWT thread
+  private val document_0 = session.begin_document(buffer.getName)
+
+  private val change_0 = new Change(document_0.id, None, Nil)  // FIXME !?
+  private var _changes = List(change_0)   // owned by Swing thread
   def changes = _changes
   private var current_change = change_0
 

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 15:33:39 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 20:40:08 2009 +0100
@@ -262,7 +262,7 @@
 
   /* activation */
 
-  def activate()
+  private def activate()
   {
     text_area.addCaretListener(selected_state_controller)
     text_area.addLeftOfScrollBar(overview)
@@ -271,7 +271,7 @@
     session.command_change += command_change_actor
   }
 
-  def deactivate()
+  private def deactivate()
   {
     session.command_change -= command_change_actor
     command_change_actor !? Exit

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 29 15:33:39 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 29 20:40:08 2009 +0100
@@ -101,13 +101,10 @@
 
   def activate_buffer(buffer: Buffer)
   {
+    session.start(Isabelle.isabelle_args())
     val model = Document_Model.init(session, buffer)
     for (text_area <- jedit_text_areas(buffer))
       Document_View.init(model, text_area)
-
-    session.start(Isabelle.isabelle_args())
-    // FIXME theory_view.activate()
-    session.begin_document(buffer.getName)
   }
 
   def deactivate_buffer(buffer: Buffer)

--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 29 15:33:39 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 29 20:40:08 2009 +0100
@@ -30,7 +30,7 @@
       "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
 
-  def empty(id: String): Proof_Document =
+  def empty(id: Isar_Document.Document_ID): Proof_Document =
     new Proof_Document(id, Linear_Set(), Map(), Linear_Set(), Map())
 
   type StructureChange = List[(Option[Command], Option[Command])]
@@ -38,11 +38,11 @@
 
 
 class Proof_Document(
-  val id: String,
+  val id: Isar_Document.Document_ID,
   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_State])   // FIXME immutable
+  var states: Map[Command, Command_State])   // FIXME immutable, eliminate!?
 {
   import Proof_Document.StructureChange
 

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Tue Dec 29 15:33:39 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Tue Dec 29 20:40:08 2009 +0100
@@ -27,6 +27,7 @@
 
   private case class Start(args: List[String])
   private case object Stop
+  private case class Begin_Document(path: String)
 
   @volatile private var _syntax = new Outer_Syntax(system.symbols)
   def syntax(): Outer_Syntax = _syntax
@@ -48,7 +49,14 @@
           if (prover != null)
             prover.kill
           prover_ready = false
-          
+
+        case Begin_Document(path: String) if prover_ready =>
+          val id = create_id()
+          val doc = Proof_Document.empty(id)
+          documents += (id -> doc)
+          prover.begin_document(id, path)
+          reply(doc)
+        
         case change: Change if prover_ready =>
           handle_change(change)
 
@@ -87,38 +95,35 @@
 
   @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
-  val document_0 = Proof_Document.empty(create_id())  // FIXME fresh id (!??)
-  @volatile private var document_versions = List(document_0)
+  @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]()
 
+  def state(id: Isar_Document.State_ID): Option[Command_State] = states.get(id)
   def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
-  def document(id: Isar_Document.Document_ID): Option[Proof_Document] =
-    document_versions.find(_.id == id)
+  def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id)
 
 
   /* document changes */
 
-  def begin_document(path: String)
-  {
-    prover.begin_document(document_0.id, path)   // FIXME fresh document!?!
-  }
+  def begin_document(path: String): Proof_Document =
+    (session_actor !? Begin_Document(path)).asInstanceOf[Proof_Document]
 
   private def handle_change(change: Change)
   {
     val old = document(change.parent.get.id).get
     val (doc, changes) = old.text_changed(this, change)
-    document_versions ::= doc
 
     val id_changes = changes map {
       case (c1, c2) =>
-        (c1.map(_.id).getOrElse(document_0.id),
+        (c1.map(_.id).getOrElse(""),
          c2 match {
             case None => None
-            case Some(command) =>
+            case Some(command) =>  // FIXME clarify -- may reuse existing commands!??
               commands += (command.id -> command)
               prover.define_command(command.id, system.symbols.encode(command.content))
               Some(command.id)
           })
     }
+    documents += (doc.id -> doc)
     prover.edit_document(old.id, doc.id, id_changes)
 
     document_change.event(doc)
@@ -143,7 +148,8 @@
         elem match {
           // document edits
           case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
-            document_versions.find(_.id == doc_id) match {
+            document(doc_id) match {
+              case None =>  // FIXME clarify
               case Some(doc) =>
                 for {
                   XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
@@ -158,7 +164,6 @@
                     case None =>
                   }
                 }
-              case None =>
             }
 
           // command and keyword declarations