removed unused Session.prover_logic;
slightly more robust Session.start/stop;
added Session.create_id (formerly in Isabelle_System);
Change/Command/Proof_Document: uniform id value, not implicity creation;
eliminated Proof_Document.is_command_keyword -- plain method via explicit session;

--- a/src/Tools/jEdit/src/proofdocument/command.scala	Thu Dec 10 22:15:19 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala	Fri Dec 11 22:25:28 2009 +0100
@@ -51,12 +51,12 @@
 
 
 class Command(
+    val id: String,
     val tokens: List[Token],
     val starts: Map[Token, Int]) extends Accumulator
 {
   require(!tokens.isEmpty)
 
-  val id = Isabelle.system.id()
   override def hashCode = id.hashCode
 
 

--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Thu Dec 10 22:15:19 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Fri Dec 11 22:25:28 2009 +0100
@@ -32,44 +32,39 @@
       "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
 
-  val empty =
-    new Proof_Document(isabelle.jedit.Isabelle.system.id(),
-      Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
+  def empty(id: String): Proof_Document =
+    new Proof_Document(id, Linear_Set(), Map(), Linear_Set(), Map())
 
   type StructureChange = List[(Option[Command], Option[Command])]
+}
 
-}
 
 class Proof_Document(
   val id: String,
   val tokens: Linear_Set[Token],
   val token_start: Map[Token, Int],
   val commands: Linear_Set[Command],
-  var states: Map[Command, Command_State],   // FIXME immutable
-  is_command_keyword: String => Boolean)
+  var states: Map[Command, Command_State])   // FIXME immutable
 {
   import Proof_Document.StructureChange
 
-  def set_command_keyword(f: String => Boolean): Proof_Document =
-    new Proof_Document(id, tokens, token_start, commands, states, f)
-
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
 
   
   /** token view **/
 
-  def text_changed(change: Change): (Proof_Document, StructureChange) =
+  def text_changed(session: Session, change: Change): (Proof_Document, StructureChange) =
   {
     def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = {
       val (doc, chgs) = doc_chgs
-      val (new_doc, chg) = doc.text_edit(edit, change.id)
+      val (new_doc, chg) = doc.text_edit(session, edit, change.id)
       (new_doc, chgs ++ chg)
     }
     ((this, Nil: StructureChange) /: change.edits)(edit_doc)
   }
 
-  def text_edit(e: Edit, id: String): (Proof_Document, StructureChange) =
+  def text_edit(session: Session, e: Edit, id: String): (Proof_Document, StructureChange) =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {
@@ -119,7 +114,7 @@
 
     while (matcher.find() && invalid_tokens != Nil) {
 			val kind =
-        if (is_command_keyword(matcher.group))
+        if (session.is_command_keyword(matcher.group))
           Token.Kind.COMMAND_START
         else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
           Token.Kind.COMMENT
@@ -143,7 +138,7 @@
     }
     val insert = new_tokens.reverse
     val new_token_list = begin ::: insert ::: old_suffix
-    token_changed(id, begin.lastOption, insert,
+    token_changed(session, id, begin.lastOption, insert,
       old_suffix.firstOption, new_token_list, start)
   }
 
@@ -151,6 +146,7 @@
   /** command view **/
 
   private def token_changed(
+    session: Session,
     new_id: String,
     before_change: Option[Token],
     inserted_tokens: List[Token],
@@ -192,7 +188,7 @@
         case t :: ts =>
           val (cmd, rest) =
             ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
-          new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
+          new Command(session.create_id(), t :: cmd, new_token_start) :: tokens_to_commands(rest)
       }
     }
 
@@ -236,7 +232,7 @@
 
     val doc =
       new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset,
-        states -- removed_commands, is_command_keyword)
+        states -- removed_commands)
 
     val removes =
       for (cmd <- removed_commands) yield (cmd_before_change -> None)

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Thu Dec 10 22:15:19 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Fri Dec 11 22:25:28 2009 +0100
@@ -12,13 +12,18 @@
 
 class Session(system: Isabelle_System)
 {
+  /* unique ids */
+
+  private var id_count: BigInt = 0
+  def create_id(): String = synchronized { id_count += 1; "j" + id_count }
+
+
   /* main actor */
 
   private case class Start(logic: String)
   private case object Stop
 
   private var prover: Isabelle_Process with Isar_Document = null
-  private var prover_logic = ""
   private var prover_ready = false
 
   private val session_actor = actor {
@@ -26,20 +31,17 @@
       react {
         case Start(logic) =>
           if (prover == null) {
-            // FIXME only once
-            prover =  // FIXME rebust error handling (via results)
-              new Isabelle_Process(system, self,   // FIXME improve options
+            prover =
+              new Isabelle_Process(system, self,   // FIXME avoid hardwired options
                   "-m", "xsymbols", "-m", "no_brackets", "-m", "no_type_brackets", logic)
                 with Isar_Document
-            prover_logic = logic
             reply(())
           }
 
         case Stop =>
           if (prover != null)
             prover.kill
-          prover = null   // FIXME later (via results)!?
-          prover_ready = false // FIXME !??
+          prover_ready = false
           
         case change: Change if prover_ready =>
           handle_change(change)
@@ -86,14 +88,14 @@
   @volatile private var _completion = new Completion + system.symbols
   def completion() = _completion
 
+  def is_command_keyword(s: String): Boolean = command_decls().contains(s)
+
 
   /* document state information */
 
   @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.
-    set_command_keyword((s: String) => command_decls().contains(s))  // FIXME !?
+  val document_0 = Proof_Document.empty(create_id())  // FIXME fresh id (!??)
   @volatile private var document_versions = List(document_0)
 
   def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
@@ -105,13 +107,13 @@
 
   def begin_document(path: String)
   {
-    prover.begin_document(document_0.id, path)   // FIXME fresh id!?!
+    prover.begin_document(document_0.id, path)   // FIXME fresh document!?!
   }
 
   def handle_change(change: Change)
   {
     val old = document(change.parent.get.id).get
-    val (doc, changes) = old.text_changed(change)
+    val (doc, changes) = old.text_changed(this, change)
     document_versions ::= doc
 
     val id_changes = changes map {
@@ -181,12 +183,14 @@
               // process ready (after initialization)
               case XML.Elem(Markup.READY, _, _) => prover_ready = true
 
-              case _ =>
+            case _ =>
             }
           }
         case _ =>
       }
       //}}}
     }
+    else if (result.kind == Isabelle_Process.Kind.EXIT)
+      prover = null
   }
 }

--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala	Thu Dec 10 22:15:19 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Fri Dec 11 22:25:28 2009 +0100
@@ -67,7 +67,7 @@
 
   private val edits_delay = Swing_Thread.delay_last(300) {
     if (!edits.isEmpty) {
-      val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
+      val change = new Change(session.create_id(), Some(current_change), edits.toList)
       _changes ::= change
       session.input(change)
       current_change = change