ProofDocument without state
handle text-events via actor

--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Thu Mar 05 16:40:49 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sun Mar 08 23:03:49 2009 +0100
@@ -9,7 +9,7 @@
 
 import isabelle.prover.{Prover, Command}
 import isabelle.renderer.UserAgent
-
+import isabelle.proofdocument.DocumentActor
 
 import org.w3c.dom.Document
 
@@ -39,9 +39,11 @@
     val buffer = view.getBuffer
     val dir = buffer.getDirectory
 
-    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)
+    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.activate
 
     //register output-view

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Mar 05 16:40:49 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Mar 08 23:03:49 2009 +0100
@@ -8,6 +8,7 @@
 
 package isabelle.jedit
 
+import scala.actors.Actor
 
 import isabelle.proofdocument.Text
 import isabelle.prover.{Prover, Command}
@@ -38,8 +39,8 @@
 }
 
 
-class TheoryView (text_area: JEditTextArea)
-    extends TextAreaExtension with Text with BufferListener {
+class TheoryView (text_area: JEditTextArea, document_actor: Actor)
+    extends TextAreaExtension with BufferListener {
 
   private val buffer = text_area.getBuffer
   private val prover = Isabelle.prover_setup(buffer).get.prover
@@ -88,7 +89,7 @@
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
     update_styles
-    changes.event(new Text.Change(0,buffer.getText(0, buffer.getLength),0))
+    document_actor ! new Text.Change(0,buffer.getText(0, buffer.getLength),0)
   }
 
   def deactivate() = {
@@ -185,19 +186,11 @@
     gfx.setColor(saved_color)
   }
 
-
-  /* Text methods */
-
-  def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
-  def length = buffer.getLength
-  val changes = new EventBus[Text.Change]
-
-
   /* BufferListener methods */
 
   private def commit {
     if (col != null)
-      changes.event(col)
+      document_actor ! col
     col = null
     if (col_timer.isRunning())
       col_timer.stop()

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/DocumentActor.scala	Sun Mar 08 23:03:49 2009 +0100
@@ -0,0 +1,35 @@
+/*
+ * 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 05 16:40:49 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sun Mar 08 23:03:49 2009 +0100
@@ -2,12 +2,15 @@
  * Document as list of commands, consisting of lists of tokens
  *
  * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
  * @author Makarius
  */
 
 package isabelle.proofdocument
 
 import scala.collection.mutable.ListBuffer
+import scala.actors.Actor
+import scala.actors.Actor._
 import java.util.regex.Pattern
 import isabelle.prover.{Prover, Command}
 import isabelle.utils.LinearSet
@@ -37,24 +40,24 @@
 
 }
 
-class ProofDocument(text: Text, is_command_keyword: String => Boolean)
+class ProofDocument(val tokens: LinearSet[Token],
+                    val commands: LinearSet[Command],
+                    val active: Boolean,
+                    is_command_keyword: String => Boolean,
+                    structural_changes: EventBus[StructureChange])
 {
-  private var active = false
-  def activate() {
-    if (!active) {
-      active = true
-      text_changed(new Text.Change(0, content, content.length))
-    }
-  }
 
-  text.changes += (change => text_changed(change))
+  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 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)
 
-  var tokens = LinearSet.empty[Token]
-  var commands = LinearSet.empty[Command]
   def content = Token.string_from_tokens(List() ++ tokens)
   /** token view **/
 
-  private def text_changed(change: Text.Change)
+  def text_changed(change: Text.Change): ProofDocument = 
   {
     val tokens = List() ++ this.tokens
     val (begin, remaining) = tokens.span(_.stop < change.start)
@@ -100,18 +103,17 @@
       }
     }
     val insert = new_tokens.reverse
-    this.tokens = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
+    val new_tokenset = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
 
     token_changed(begin.lastOption,
                   insert,
                   removed,
+                  new_tokenset,
                   old_suffix.firstOption)
   }
   
   /** command view **/
 
-  val structural_changes = new EventBus[StructureChange]
-
   def find_command_at(pos: Int): Command = {
     for (cmd <- commands) { if (pos < cmd.stop) return cmd }
     return null
@@ -120,7 +122,8 @@
   private def token_changed(before_change: Option[Token],
                             inserted_tokens: List[Token],
                             removed_tokens: List[Token],
-                            after_change: Option[Token])
+                            new_tokenset: LinearSet[Token],
+                            after_change: Option[Token]): ProofDocument =
   {
     val commands = List() ++ this.commands
     val (begin, remaining) =
@@ -164,8 +167,9 @@
     val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
     System.err.println("new_commands: " + new_commands)
 
-    this.commands = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
+    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)
   }
 }

--- a/src/Tools/jEdit/src/proofdocument/Text.scala	Thu Mar 05 16:40:49 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Sun Mar 08 23:03:49 2009 +0100
@@ -11,8 +11,4 @@
   case class Change(start: Int, val added: String, val removed: Int) {
     override def toString = "start: " + start + " added: " + added + " removed: " + removed
   }
-}
-
-trait Text {
-  def changes: EventBus[Text.Change]
-}
+}
\ No newline at end of file

--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Mar 05 16:40:49 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Mar 08 23:03:49 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.{DocumentActor, ProofDocument, Text, Token}
 import isabelle.IsarDocument
 
 
@@ -81,8 +81,8 @@
   val activated = new EventBus[Unit]
   val command_info = new EventBus[Command]
   val output_info = new EventBus[String]
-  var document: ProofDocument = null
-
+  var document_actor: DocumentActor = null
+  def document = document_actor.get
 
   def command_change(c: Command) = Swing.now { command_info.event(c) }
 
@@ -101,12 +101,7 @@
       Swing.now { output_info.event(result.result) }
     else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) {  // FIXME !?
       initialized = true
-      Swing.now {
-        if (document != null) {
-          document.activate()
-          activated.event(())
-        }
-      }
+      Swing.now { document_actor ! DocumentActor.Activate }
     }
     else {
       result.kind match {
@@ -191,11 +186,16 @@
     }
   }
 
-  def set_document(text: Text, path: String) {
-    this.document = new ProofDocument(text, command_decls.contains(_))
+  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))
 
-    document.structural_changes += (changes => if(initialized){
+    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)})
     })