# HG changeset patch
# User wenzelm
# Date 1252442281 -7200
# Node ID b1079c3ba1da0f26742f54d68a1bc5d70f5ed9a3
# Parent  740755bfef08e36090ef97824c9083bbbdff964b
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
TheoryView: simplified change_receiver, only for local purposes (via command_change);
Accumulator: message requires explicit prover context for now;

diff -r 740755bfef08 -r b1079c3ba1da src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala
--- a/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala	Mon Sep 07 23:54:53 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala	Tue Sep 08 22:38:01 2009 +0200
@@ -16,15 +16,18 @@
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
-class BrowseVersionDockable(view : View, position : String) extends FlowPanel
+class BrowseVersionDockable(view: View, position: String) extends FlowPanel
 {
-
-  def get_versions() =
-    Isabelle.prover_setup(view.getBuffer).map(_.theory_view.changes).getOrElse(Nil)
-
   if (position == DockableWindowManager.FLOATING)
     preferredSize = new Dimension(500, 250)
 
+  def prover_setup(): Option[ProverSetup] = Isabelle.prover_setup(view.getBuffer)
+  def get_versions() =
+    prover_setup() match {
+      case None => Nil
+      case Some(setup) => setup.theory_view.changes
+    }
+
   val list = new ListView[Change]
   list.fixedCellWidth = 500
   list.listData = get_versions()
@@ -33,15 +36,8 @@
   listenTo(list.selection)
   reactions += {
     case ListSelectionChanged(source, range, false) =>
-      Swing_Thread.now {
-        Isabelle.prover_setup(view.getBuffer).map(_.
-          theory_view.set_version(list.listData(range.start)))
-      }
-  }
+        prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
+    }
 
-  private var num_changes = 0
-  Isabelle.plugin.document_change += {_ =>
-    list.listData = get_versions()
-  }
-
+  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
 }
diff -r 740755bfef08 -r b1079c3ba1da src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Sep 07 23:54:53 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Sep 08 22:38:01 2009 +0200
@@ -101,8 +101,6 @@
   /* event buses */
 
   val state_update = new Event_Bus[Command]
-  val command_change = new Event_Bus[Command]
-  val document_change = new Event_Bus[ProofDocument]
 
 
   /* selected state */
diff -r 740755bfef08 -r b1079c3ba1da src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Sep 07 23:54:53 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Sep 08 22:38:01 2009 +0200
@@ -44,30 +44,18 @@
 
   /* prover setup */
 
-  val change_receiver: Actor = new Actor {
-    def act() {
-      loop {
-        react {
-          case c: Command =>
-            actor { Isabelle.plugin.command_change.event(c) }
-            if (current_document().commands.contains(c))
-            Swing_Thread.later {
-              // repaint if buffer is active
-              if (text_area.getBuffer == buffer) {
-                update_syntax(c)
-                invalidate_line(c)
-                phase_overview.repaint()
-              }
-            }
-          case d: ProofDocument =>
-            actor { Isabelle.plugin.document_change.event(d) }
-          case bad => System.err.println("change_receiver: ignoring bad message " + bad)
+  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
+
+  prover.command_change += ((command: Command) =>
+    if (current_document().commands.contains(command))
+      Swing_Thread.later {
+        // repaint if buffer is active
+        if (text_area.getBuffer == buffer) {
+          update_syntax(command)
+          invalidate_line(command)
+          phase_overview.repaint()
         }
-      }
-    }
-  }
-
-  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic(), change_receiver)
+      })
   
 
   /* activation */
@@ -325,7 +313,6 @@
 
   /* init */
 
-  change_receiver.start()
   prover.start()
 
   edits += Insert(0, buffer.getText(0, buffer.getLength))
diff -r 740755bfef08 -r b1079c3ba1da src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Sep 07 23:54:53 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Sep 08 22:38:01 2009 +0200
@@ -35,8 +35,7 @@
 
   val empty =
     new ProofDocument(isabelle.jedit.Isabelle.system.id(),
-      Linear_Set(), Map(), Linear_Set(), Map(), _ => false,
-      actor(loop(react{case _ =>}))) // ignoring actor
+      Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
 
   type StructureChange = List[(Option[Command], Option[Command])]
 
@@ -48,16 +47,12 @@
   val token_start: Map[Token, Int],
   val commands: Linear_Set[Command],
   var states: Map[Command, Command_State],   // FIXME immutable
-  is_command_keyword: String => Boolean,
-  change_receiver: Actor)
+  is_command_keyword: String => Boolean)
 {
   import ProofDocument.StructureChange
 
   def set_command_keyword(f: String => Boolean): ProofDocument =
-    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)
+    new ProofDocument(id, tokens, token_start, commands, states, f)
 
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
@@ -198,7 +193,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, change_receiver) :: tokens_to_commands(rest)
+          new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
       }
     }
 
@@ -240,7 +235,7 @@
 
     val doc =
       new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
-        states -- removed_commands, is_command_keyword, change_receiver)
+        states -- removed_commands, is_command_keyword)
 
     val removes =
       for (cmd <- removed_commands) yield (cmd_before_change -> None)
diff -r 740755bfef08 -r b1079c3ba1da src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Sep 07 23:54:53 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Sep 08 22:38:01 2009 +0200
@@ -27,7 +27,8 @@
   override def act() {
     loop {
       react {
-        case message: XML.Tree => _state += message
+        case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
+        case bad => System.err.println("prover: ignoring bad message " + bad)
       }
     }
   }
@@ -52,16 +53,13 @@
 
 class Command(
     val tokens: List[Token],
-    val starts: Map[Token, Int],
-  change_receiver: Actor) extends Accumulator
+    val starts: Map[Token, Int]) extends Accumulator
 {
   require(!tokens.isEmpty)
 
   val id = Isabelle.system.id()
   override def hashCode = id.hashCode
 
-  def changed() = change_receiver ! this
-
 
   /* content */
 
diff -r 740755bfef08 -r b1079c3ba1da src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Sep 07 23:54:53 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Sep 08 22:38:01 2009 +0200
@@ -17,10 +17,9 @@
 import isabelle.proofdocument.{ProofDocument, Change, Token}
 
 
-class Prover(isabelle_system: Isabelle_System, logic: String, change_receiver: Actor)
-  extends Actor
+class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor
 {
-  /* message handling */
+  /* incoming messages */
   
   private var prover_ready = false
 
@@ -35,6 +34,12 @@
   }
 
 
+  /* outgoing messages */
+  
+  val command_change = new Event_Bus[Command]
+  val document_change = new Event_Bus[ProofDocument]
+
+
   /* prover process */
 
   private val process =
@@ -62,8 +67,7 @@
   @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   val document_0 =
     ProofDocument.empty.
-      set_command_keyword((s: String) => command_decls().contains(s)).
-      set_change_receiver(change_receiver)
+      set_command_keyword((s: String) => command_decls().contains(s))
   @volatile private var document_versions = List(document_0)
 
   def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
@@ -89,7 +93,7 @@
 
     val message = Isabelle_Process.parse_message(isabelle_system, result)
 
-    if (state.isDefined) state.get ! message
+    if (state.isDefined) state.get ! (this, message)
     else result.kind match {
 
       case Isabelle_Process.Kind.STATUS =>
@@ -124,7 +128,7 @@
                       val state = new Command_State(cmd)
                       states += (state_id -> state)
                       doc.states += (cmd -> state)
-                      cmd.changed()
+                      command_change.event(cmd)
                     }
                   }
                 case XML.Elem(kind, attr, body) =>
@@ -134,7 +138,7 @@
                   val markup_id = Position.id_of(attr)
                   val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
                   if (outer && begin.isDefined && end.isDefined && markup_id.isDefined)
-                    commands.get(markup_id.get).map (cmd => cmd ! message)
+                    commands.get(markup_id.get).map(cmd => cmd ! (this, message))
                 case _ =>
                 //}}}
               }
@@ -154,7 +158,7 @@
     val (doc, structure_change) = old.text_changed(change)
     document_versions ::= doc
     edit_document(old, doc, structure_change)
-    change_receiver ! doc
+    document_change.event(doc)
   }
 
   def set_document(path: String) {
diff -r 740755bfef08 -r b1079c3ba1da src/Tools/jEdit/src/prover/State.scala
--- a/src/Tools/jEdit/src/prover/State.scala	Mon Sep 07 23:54:53 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala	Tue Sep 08 22:38:01 2009 +0200
@@ -70,7 +70,7 @@
 
   /* message dispatch */
 
-  def + (message: XML.Tree): State =
+  def + (prover: Prover, message: XML.Tree): State =
   {
     val changed: State =
       message match {
@@ -111,7 +111,7 @@
             })
         case _ => add_result(message)
       }
-    if (!(this eq changed)) command.changed()
+    if (!(this eq changed)) prover.command_change.event(command)
     changed
   }
 }