Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
added actor to TheoryView, receiving updates of Commands (removed EventBus command_info);
Prover.edit_document from Makarius 'broken' repository;
LinearSet: fixed prev

--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Thu Mar 19 16:18:57 2009 +0100
@@ -7,8 +7,7 @@
 
 package isabelle.jedit
 
-import isabelle.proofdocument.ProofDocument
-import isabelle.prover.{Command, MarkupNode}
+import isabelle.prover.{Command, MarkupNode, Prover}
 import isabelle.Markup
 
 import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -68,7 +67,7 @@
 
 }
 
-class DynamicTokenMarker(buffer: JEditBuffer, document: ProofDocument) extends TokenMarker {
+class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker {
 
   override def markTokens(prev: TokenMarker.LineContext,
     handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
@@ -83,7 +82,7 @@
 
     var next_x = start
     for {
-      command <- document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
+      command <- prover.document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
       markup <- command.root_node.flatten
       if(to(markup.abs_stop) > start)
       if(to(markup.abs_start) < stop)

--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Thu Mar 19 16:18:57 2009 +0100
@@ -24,7 +24,6 @@
   var textarea : JEditTextArea = null
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
-  prover.command_info += (_ => repaint_delay.delay_or_ignore())
 
   setRequestFocusEnabled(false);
 

--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Thu Mar 19 16:18:57 2009 +0100
@@ -9,7 +9,6 @@
 
 import isabelle.prover.{Prover, Command}
 import isabelle.renderer.UserAgent
-import isabelle.proofdocument.DocumentActor
 
 import org.w3c.dom.Document
 
@@ -35,15 +34,13 @@
 
   def activate(view: View) {
     prover = new Prover(Isabelle.system, Isabelle.default_logic)
-
+    prover.start() //start actor
     val buffer = view.getBuffer
-    val dir = buffer.getDirectory
+    val path = buffer.getPath
 
-    val document_actor = new DocumentActor
-    document_actor.start
-    theory_view = new TheoryView(view.getTextArea, document_actor)
-    prover.set_document(document_actor,
-      if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
+    theory_view = new TheoryView(view.getTextArea, prover)
+    prover.set_document(theory_view.change_receiver,
+    if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path)
     theory_view.activate
 
     //register output-view

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Mar 19 16:18:57 2009 +0100
@@ -87,7 +87,7 @@
     phase_overview.textarea = text_area
     text_area.addLeftOfScrollBar(phase_overview)
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
-    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
+    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
     update_styles
     document_actor ! new Text.Change(0,buffer.getText(0, buffer.getLength),0)
   }
@@ -102,7 +102,17 @@
   /* painting */
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
-  prover.command_info += (_ => repaint_delay.delay_or_ignore())
+  
+  val change_receiver = scala.actors.Actor.actor {
+    scala.actors.Actor.loop {
+      scala.actors.Actor.react {
+        case _ => {
+            repaint_delay.delay_or_ignore()
+            phase_overview.repaint_delay.delay_or_ignore()
+        }
+      }
+    }
+  }.start
 
   def from_current (pos: Int) =
     if (col != null && col.start <= pos)

--- a/src/Tools/jEdit/src/proofdocument/DocumentActor.scala	Thu Mar 19 13:16:07 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-/*
- * Managing changes on ProofDocuments via Actors
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.proofdocument
-
-import scala.actors.Actor
-import scala.actors.Actor._
-import isabelle.utils.LinearSet
-
-object DocumentActor {
-  case class Activate
-  case class SetEventBus(bus: EventBus[StructureChange])
-  case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
-}
-class DocumentActor extends Actor {
-  private var versions = List(
-    new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false, new EventBus))
-
-  def get = versions.head
-  
-  def act() {
-    import DocumentActor._
-    loop {
-      react {
-        case Activate => versions ::= versions.head.activate
-        case SetEventBus(bus) => versions ::= versions.head.set_event_bus(bus)
-        case SetIsCommandKeyword(f) => versions ::= versions.head.set_command_keyword(f)
-        case change: Text.Change => versions ::= versions.head.text_changed(change)
-      }
-    }
-  }
-}

--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Mar 19 16:18:57 2009 +0100
@@ -38,26 +38,28 @@
       "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
 
+ val empty = new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false)
+
 }
 
 class ProofDocument(val tokens: LinearSet[Token],
                     val commands: LinearSet[Command],
                     val active: Boolean,
-                    is_command_keyword: String => Boolean,
-                    structural_changes: EventBus[StructureChange])
+                    is_command_keyword: String => Boolean)
 {
 
-  def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword, structural_changes)
-  def activate: ProofDocument = text_changed(new Text.Change(0, content, content.length)).mark_active
+  def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword)
+  def activate: (ProofDocument, StructureChange) = {
+    val (doc, change) = text_changed(new Text.Change(0, content, content.length))
+    return (doc.mark_active, change)
+  }
   def set_command_keyword(f: String => Boolean): ProofDocument =
-    new ProofDocument(tokens, commands, active, f, structural_changes)
-  def set_event_bus(bus: EventBus[StructureChange]): ProofDocument =
-    new ProofDocument(tokens, commands, active, is_command_keyword, bus)
+    new ProofDocument(tokens, commands, active, f)
 
   def content = Token.string_from_tokens(List() ++ tokens)
   /** token view **/
 
-  def text_changed(change: Text.Change): ProofDocument = 
+  def text_changed(change: Text.Change): (ProofDocument, StructureChange) =
   {
     val tokens = List() ++ this.tokens
     val (begin, remaining) = tokens.span(_.stop < change.start)
@@ -123,7 +125,7 @@
                             inserted_tokens: List[Token],
                             removed_tokens: List[Token],
                             new_tokenset: LinearSet[Token],
-                            after_change: Option[Token]): ProofDocument =
+                            after_change: Option[Token]): (ProofDocument, StructureChange) =
   {
     val commands = List() ++ this.commands
     val (begin, remaining) =
@@ -163,13 +165,13 @@
       }
     }
 
-    System.err.println("ins_tokens: " + inserted_tokens)
     val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
-    System.err.println("new_commands: " + new_commands)
 
     val new_commandset = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
     val before = begin match {case Nil => None case _ => Some (begin.last)}
-    structural_changes.event(new StructureChange(before, new_commands, removed))
-    new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword, structural_changes)
+
+    val change = new StructureChange(before, new_commands, removed)
+    val doc = new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword)
+    return (doc, change)
   }
 }

--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Mar 19 16:18:57 2009 +0100
@@ -12,23 +12,31 @@
 import scala.collection.mutable
 import scala.collection.immutable.{TreeSet}
 
+import scala.actors.Actor
+import scala.actors.Actor._
+
 import org.gjt.sp.util.Log
 
 import isabelle.jedit.Isabelle
-import isabelle.proofdocument.{DocumentActor, ProofDocument, Text, Token}
+import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token}
 import isabelle.IsarDocument
 
+object ProverEvents {
+  case class Activate
+  case class SetEventBus(bus: EventBus[StructureChange])
+  case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
+}
 
-class Prover(isabelle_system: IsabelleSystem, logic: String)
+class Prover(isabelle_system: IsabelleSystem, logic: String) extends Actor
 {
   /* prover process */
 
-  private var process: Isar = null
+  private var process: Isar with IsarDocument= null
 
   {
     val results = new EventBus[IsabelleProcess.Result] + handle_result
     results.logger = Log.log(Log.ERROR, null, _)
-    process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
+    process = new Isar(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument
   }
 
   def stop() { process.kill }
@@ -39,7 +47,10 @@
   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 var document_versions = List((document0, ProofDocument.empty))
+
+  def get_id = document_versions.head._1
+  def document = document_versions.head._2
 
   private var initialized = false
 
@@ -79,12 +90,10 @@
   /* event handling */
 
   val activated = new EventBus[Unit]
-  val command_info = new EventBus[Command]
   val output_info = new EventBus[String]
-  var document_actor: DocumentActor = null
-  def document = document_actor.get
-
-  def command_change(c: Command) = Swing.now { command_info.event(c) }
+  var change_receiver = null: Actor
+  
+  def command_change(c: Command) = this ! c
 
   private def handle_result(result: IsabelleProcess.Result)
   {
@@ -101,18 +110,21 @@
       Swing.now { output_info.event(result.result) }
     else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) {  // FIXME !?
       initialized = true
-      Swing.now { document_actor ! DocumentActor.Activate }
+      Swing.now { this ! ProverEvents.Activate }
     }
     else {
       result.kind match {
 
         case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
-          | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR
-        if command != null =>
-          if (result.kind == IsabelleProcess.Kind.ERROR)
-            command.status = Command.Status.FAILED
-          command.add_result(running, process.parse_message(result))
-          command_change(command)
+          | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR =>
+          if (command != null) {
+            if (result.kind == IsabelleProcess.Kind.ERROR)
+              command.status = Command.Status.FAILED
+            command.add_result(running, process.parse_message(result))
+            command_change(command)
+          } else {
+            output_info.event(result.toString)
+          }
 
         case IsabelleProcess.Kind.STATUS =>
           //{{{ handle all kinds of status messages here
@@ -136,13 +148,13 @@
                         <- 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)
-                    }
+                        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)
+                      }
 
                   // command status
                   case XML.Elem(Markup.UNPROCESSED, _, _)
@@ -170,9 +182,10 @@
                       if (command == null) commands.getOrElse(markup_id, null)
                       // inner syntax: id from props
                       else command
-                    if (cmd != null)
+                    if (cmd != null) {
                       cmd.root_node.insert(cmd.node_from(kind, begin, end))
-
+                      command_change(cmd)
+                    }
                   case _ =>
                   //}}}
                 }
@@ -186,33 +199,59 @@
     }
   }
 
-  def set_document(document_actor: isabelle.proofdocument.DocumentActor, path: String) {
-    val structural_changes = new EventBus[isabelle.proofdocument.StructureChange]
-
-    this.document_actor = document_actor
-    document_actor ! DocumentActor.SetEventBus(structural_changes)
-    document_actor ! DocumentActor.SetIsCommandKeyword(command_decls.contains)
-
-    process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
-
-    structural_changes += (changes => if(initialized){
-      for (cmd <- changes.removed_commands) remove(cmd)
-      changes.added_commands.foldLeft (changes.before_change) ((p, c) => {send(p, c); Some(c)})
-    })
+  def act() {
+    import ProverEvents._
+    loop {
+      react {
+        case Activate => {
+            val (doc, structure_change) = document.activate
+            val old_id = get_id
+            val doc_id = Isabelle.plugin.id()
+            document_versions ::= (doc_id, doc)
+            edit_document(old_id, doc_id, structure_change)
+        }
+        case SetIsCommandKeyword(f) => {
+            val old_id = get_id
+            val doc_id = Isabelle.plugin.id()
+            document_versions ::= (doc_id, document.set_command_keyword(f))
+            edit_document(old_id, doc_id, StructureChange(None, Nil, Nil))
+        }
+        case change: Text.Change => {
+            val (doc, structure_change) = document.text_changed(change)
+            val old_id = get_id
+            val doc_id = Isabelle.plugin.id()
+            document_versions ::= (doc_id, doc)
+            edit_document(old_id, doc_id, structure_change)
+        }
+        case command: Command => {
+            //state of command has changed
+            change_receiver ! command
+        }
+      }
+    }
+  }
+  
+  def set_document(change_receiver: Actor, path: String) {
+    this.change_receiver = change_receiver
+    this ! ProverEvents.SetIsCommandKeyword(command_decls.contains)
+    process.ML("()")  // FIXME force initial writeln
+    process.begin_document(document0, path)
   }
 
-  private def send(prev: Option[Command], cmd: Command) {
-    cmd.status = Command.Status.UNPROCESSED
-    commands.put(cmd.id, cmd)
-
-    val content = isabelle_system.symbols.encode(cmd.content)
-    process.create_command(cmd.id, content)
-    process.insert_command(prev match {case Some(c) => c.id case None => ""}, cmd.id)
-  }
-
-  def remove(cmd: Command) {
-    commands -= cmd.id
-    if (cmd.state_id != null) states -= cmd.state_id
-    process.remove_command(cmd.id)
+  private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now
+  {
+    val removes =
+      for (cmd <- changes.removed_commands) yield {
+        commands -= cmd.id
+        if (cmd.state_id != null) states -= cmd.state_id
+        (document.commands.prev(cmd).map(_.id).getOrElse(document0)) -> None
+      }
+    val inserts =
+      for (cmd <- changes.added_commands) yield {
+        commands += (cmd.id -> cmd)
+        process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
+        (document.commands.prev(cmd).map(_.id).getOrElse(document0)) -> Some(cmd.id)
+      }
+    process.edit_document(old_id, document_id, removes.reverse ++ inserts)
   }
 }

--- a/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 19 16:18:57 2009 +0100
@@ -34,7 +34,7 @@
   /* basic methods */
 
   def next(elem: A) = body.get(elem)
-  def prev(elem: A) = body.find(_._2 == elem).map(_._2)
+  def prev(elem: A) = body.find(_._2 == elem).map(_._1)
   override def isEmpty: Boolean = !last_elem.isDefined
   def size: Int = if (isEmpty) 0 else body.size + 1