# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID f9b71bcf2eb7e838ab7459eba178e368c212e2d8
# Parent  1a30c075c202b80dc1e73910c648c178eea62be8
Command notifies changes

diff -r 1a30c075c202 -r f9b71bcf2eb7 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -8,9 +8,11 @@
 
 package isabelle.proofdocument
 
+import scala.actors.Actor
+import scala.actors.Actor._
 import scala.collection.mutable.ListBuffer
 import java.util.regex.Pattern
-import isabelle.prover.{Prover, Command}
+import isabelle.prover.{Prover, Command, Command_State}
 import isabelle.utils.LinearSet
 
 
@@ -34,7 +36,8 @@
 
   val empty =
     new ProofDocument(isabelle.jedit.Isabelle.system.id(),
-      LinearSet(), Map(), LinearSet(), Map(), _ => false)
+      LinearSet(), Map(), LinearSet(), Map(), _ => false,
+      actor(loop(react{case _ =>}))) // ignoring actor
 
   type StructureChange = List[(Option[Command], Option[Command])]
 
@@ -46,12 +49,16 @@
   val token_start: Map[Token, Int],
   val commands: LinearSet[Command],
   var states: Map[Command, IsarDocument.State_ID],
-  is_command_keyword: String => Boolean)
+  is_command_keyword: String => Boolean,
+  change_receiver: Actor)
 {
   import ProofDocument.StructureChange
 
   def set_command_keyword(f: String => Boolean): ProofDocument =
-    new ProofDocument(id, tokens, token_start, commands, states, f)
+    new ProofDocument(id, tokens, token_start, commands, states, f, change_receiver)
+
+  def set_change_receiver(cr: Actor): ProofDocument =
+    new ProofDocument(id, tokens, token_start, commands, states, is_command_keyword, cr)
 
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
@@ -192,7 +199,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(t :: cmd, new_token_start, change_receiver) :: tokens_to_commands(rest)
       }
     }
 
@@ -233,8 +240,8 @@
         insert_after(cmd_before_change, inserted_commands)
 
     val doc =
-      new ProofDocument(new_id, new_tokenset, new_token_start,
-        new_commandset, states -- removed_commands, is_command_keyword)
+      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
+        states -- removed_commands, is_command_keyword, change_receiver)
 
     val removes =
       for (cmd <- removed_commands) yield (cmd_before_change -> None)
diff -r 1a30c075c202 -r f9b71bcf2eb7 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -8,8 +8,8 @@
 package isabelle.prover
 
 
-import javax.swing.text.Position
-import javax.swing.tree.DefaultMutableTreeNode
+import scala.actors.Actor
+import scala.actors.Actor._
 
 import scala.collection.mutable
 
@@ -31,13 +31,16 @@
 }
 
 
-class Command(val tokens: List[Token], val starts: Map[Token, Int])
+class Command(val tokens: List[Token], val starts: Map[Token, Int], chg_rec: Actor)
 {
   require(!tokens.isEmpty)
 
   val id = Isabelle.system.id()
   override def hashCode = id.hashCode
 
+  def changed() = chg_rec ! this
+
+
   /* content */
 
   override def toString = name
diff -r 1a30c075c202 -r f9b71bcf2eb7 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -92,7 +92,7 @@
 
   private def handle_result(result: Isabelle_Process.Result)
   {
-    def command_change(c: Command) = change_receiver ! c
+    def command_change(c: Command) = c.changed()
     val (state, command) =
       result.props.find(p => p._1 == Markup.ID) match {
         case None => (null, null)