preliminary/failed attempt to use the new IsarDocument access model to the prover;
misc tuning;

--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jan 27 22:23:45 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Mon Mar 02 19:17:20 2009 +0100
@@ -37,17 +37,17 @@
     prover = new Prover(Isabelle.system, Isabelle.default_logic)
     
     val buffer = view.getBuffer
-    val dir = buffer.getDirectory
+    val path = buffer.getPath
 
     theory_view = new TheoryView(view.getTextArea)
     prover.set_document(theory_view,
-        if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
+      if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path)
     theory_view.activate
 
     //register output-view
     prover.output_info += (text =>
       {
-        output_text_view.append(text)
+        output_text_view.append(text + "\n")
         val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
         //link process output if dockable is active
         if (dockable != null) {

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jan 27 22:23:45 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Mar 02 19:17:20 2009 +0100
@@ -242,14 +242,9 @@
 
 
   override def contentInserted(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
-  override def contentRemoved(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
-  override def preContentInserted(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int) =
+    start_line: Int, offset: Int, num_lines: Int, length: Int)
   {
+/*
     if (col == null)
       col = new Text.Changed(offset, length, 0)
     else if (col.start <= offset && offset <= col.start + col.added)
@@ -259,11 +254,14 @@
       col = new Text.Changed(offset, length, 0)
     }
     delay_commit()
+*/
+    changes.event(new Text.Changed(offset, length, 0))
   }
 
   override def preContentRemoved(buffer: JEditBuffer,
     start_line: Int, start: Int, num_lines: Int, removed: Int) =
   {
+/*
     if (col == null)
       col = new Text.Changed(start, 0, removed)
     else if (col.start > start + removed || start > col.start + col.added) {
@@ -281,8 +279,14 @@
       col = new Text.Changed(start min col.start, added, col.removed - add_removed)
     }
     delay_commit()
+*/
+    changes.event(new Text.Changed(start, 0, removed))
   }
 
+  override def contentRemoved(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+  override def preContentInserted(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
   override def bufferLoaded(buffer: JEditBuffer) { }
   override def foldHandlerChanged(buffer: JEditBuffer) { }
   override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }

--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jan 27 22:23:45 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Mar 02 19:17:20 2009 +0100
@@ -219,7 +219,8 @@
       else if (after_change != null)
         after_change.prev = before_change
     }
-    
+
+    System.err.println("token_changed: " + before_change + " " + after_change + " " + first_removed)
     token_changed(before_change, after_change, first_removed)
   }
   

--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jan 27 22:23:45 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Mon Mar 02 19:17:20 2009 +0100
@@ -45,7 +45,8 @@
     start = bottom_clamp max (start + offset)
     stop = bottom_clamp max (stop + offset)
   }
-  
+
+  override def toString: String = "[" + start + ":" + stop + "]"
   override def hashCode: Int = (31 + start) * 31 + stop
 
   override def equals(obj: Any): Boolean =

--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 27 22:23:45 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Mon Mar 02 19:17:20 2009 +0100
@@ -72,6 +72,7 @@
   def status = _status
   def status_=(st: Command.Status.Value) {
     if (st == Command.Status.UNPROCESSED) {
+      state_results.clear
       // delete markup
       for (child <- root_node.children) {
         child.children = Nil
@@ -85,7 +86,7 @@
 
   private val results = new mutable.ListBuffer[XML.Tree]
   private val state_results = new mutable.ListBuffer[XML.Tree]
-  def add_result(running: Boolean, tree: XML.Tree) {
+  def add_result(running: Boolean, tree: XML.Tree) = synchronized {
     (if (running) state_results else results) += tree
   }
 

--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 27 22:23:45 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Mar 02 19:17:20 2009 +0100
@@ -15,7 +15,7 @@
 import org.gjt.sp.util.Log
 
 import isabelle.jedit.Isabelle
-import isabelle.proofdocument.{ProofDocument, Text, Token}
+import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token}
 import isabelle.IsarDocument
 
 
@@ -23,12 +23,11 @@
 {
   /* prover process */
 
-  private var process: Isar = null
-
+  private val process =
   {
     val results = new EventBus[IsabelleProcess.Result] + handle_result
     results.logger = Log.log(Log.ERROR, null, _)
-    process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
+    new IsabelleProcess(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument
   }
 
   def stop() { process.kill }
@@ -36,10 +35,13 @@
   
   /* document state information */
 
-  private val states = new mutable.HashMap[IsarDocument.State_ID, Command]
-  private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command]
-  private val document0 = Isabelle.plugin.id()
-  private val document_versions = new mutable.HashSet[IsarDocument.Document_ID] + document0
+  private val states = new mutable.HashMap[IsarDocument.State_ID, Command] with
+    mutable.SynchronizedMap[IsarDocument.State_ID, Command]
+  private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
+    mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
+  private val document_id0 = Isabelle.plugin.id()
+  private var document_id = document_id0
+  private var document_versions = Set(document_id)
 
   private var initialized = false
 
@@ -48,13 +50,15 @@
 
   val decl_info = new EventBus[(String, String)]
 
-  private val keyword_decls = new mutable.HashSet[String] {
+  private val keyword_decls =
+    new mutable.HashSet[String] with mutable.SynchronizedSet[String] {
     override def +=(name: String) = {
       decl_info.event(name, OuterKeyword.MINOR)
       super.+=(name)
     }
   }
-  private val command_decls = new mutable.HashMap[String, String] {
+  private val command_decls =
+    new mutable.HashMap[String, String] with mutable.SynchronizedMap[String, String] {
     override def +=(entry: (String, String)) = {
       decl_info.event(entry)
       super.+=(entry)
@@ -84,10 +88,9 @@
   var document: ProofDocument = null
 
 
-  def command_change(c: Command) = Swing.now { command_info.event(c) }
-
-  private def handle_result(result: IsabelleProcess.Result)
+  private def handle_result(result: IsabelleProcess.Result): Unit = Swing.now
   {
+    def command_change(c: Command) = command_info.event(c)
     val (running, command) =
       result.props.find(p => p._1 == Markup.ID) match {
         case None => (false, null)
@@ -98,14 +101,12 @@
       }
 
     if (result.kind == IsabelleProcess.Kind.STDOUT || result.kind == IsabelleProcess.Kind.STDIN)
-      Swing.now { output_info.event(result.result) }
+      output_info.event(result.toString)
     else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) {  // FIXME !?
       initialized = true
-      Swing.now {
-        if (document != null) {
-          document.activate()
-          activated.event(())
-        }
+      if (document != null) {
+        document.activate()
+        activated.event(())
       }
     }
     else {
@@ -136,30 +137,35 @@
                   // document edits
                   case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
                   if document_versions.contains(doc_id) =>
+                    output_info.event(result.toString)
                     for {
                       XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
                         <- edits
-                      if (commands.contains(cmd_id))
                     } {
-                      val cmd = commands(cmd_id)
-                      if (cmd.state_id != null) states -= cmd.state_id
-                      states(cmd_id) = cmd
-                      cmd.state_id = state_id
-                      cmd.status = Command.Status.UNPROCESSED
-                      command_change(cmd)
+                      if (commands.contains(cmd_id)) {
+                        val cmd = commands(cmd_id)
+                        if (cmd.state_id != null) states -= cmd.state_id
+                        states(state_id) = cmd
+                        cmd.state_id = state_id
+                        cmd.status = Command.Status.UNPROCESSED
+                        command_change(cmd)
+                      }
                     }
 
                   // command status
                   case XML.Elem(Markup.UNPROCESSED, _, _)
                   if command != null =>
+                    output_info.event(result.toString)
                     command.status = Command.Status.UNPROCESSED
                     command_change(command)
                   case XML.Elem(Markup.FINISHED, _, _)
                   if command != null =>
+                    output_info.event(result.toString)
                     command.status = Command.Status.FINISHED
                     command_change(command)
                   case XML.Elem(Markup.FAILED, _, _)
                   if command != null =>
+                    output_info.event(result.toString)
                     command.status = Command.Status.FAILED
                     command_change(command)
 
@@ -191,32 +197,37 @@
     }
   }
 
-  def set_document(text: Text, path: String) {
-    this.document = new ProofDocument(text, command_decls.contains(_))
-    process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
-
-    document.structural_changes += (changes => {
-      for (cmd <- changes.removed_commands) remove(cmd)
-      for (cmd <- changes.added_commands) send(cmd)
-    })
+  def set_document(text: Text, path: String): Unit = Swing.now
+  {
+    document = new ProofDocument(text, command_decls.contains(_))
+    process.ML("()")  // FIXME force initial writeln
+    process.begin_document(document_id0, path)
+    document.structural_changes += edit_document
+    // FIXME !?
     if (initialized) {
       document.activate()
       activated.event(())
     }
   }
 
-  private def send(cmd: Command) {
-    cmd.status = Command.Status.UNPROCESSED
-    commands.put(cmd.id, cmd)
+  private def edit_document(changes: StructureChange) = Swing.now
+  {
+    val old_id = document_id
+    document_id = Isabelle.plugin.id()
+    document_versions += document_id
 
-    val content = isabelle_system.symbols.encode(cmd.content)
-    process.create_command(cmd.id, content)
-    process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id)
-  }
-
-  def remove(cmd: Command) {
-    commands -= cmd.id
-    if (cmd.state_id != null) states -= cmd.state_id
-    process.remove_command(cmd.id)
+    val removes =
+      for (cmd <- changes.removed_commands) yield {
+        commands -= cmd.id
+        if (cmd.state_id != null) states -= cmd.state_id
+        (if (cmd.prev == null) document_id0 else cmd.prev.id) -> None
+      }
+    val inserts =
+      for (cmd <- changes.added_commands) yield {
+        commands += (cmd.id -> cmd)
+        process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
+        (if (cmd.prev == null) document_id0 else cmd.prev.id) -> Some(cmd.id)
+      }
+    process.edit_document(old_id, document_id, removes.reverse ++ inserts)
   }
 }