--- a/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 12:12:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 16:41:33 2009 +0200
@@ -15,6 +15,7 @@
import scala.collection.mutable
import isabelle.prover.{Prover, Command}
+import isabelle.proofdocument.ProofDocument
import isabelle.Isabelle_System
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
@@ -95,11 +96,14 @@
font_changed.event(font)
}
+ /* event buses */
+
+ val state_update = new EventBus[Command]
+ val command_change = new EventBus[Command]
+ val document_change = new EventBus[ProofDocument]
/* selected state */
- val state_update = new EventBus[Command]
-
private var _selected_state: Command = null
def selected_state = _selected_state
def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 12:12:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 16:41:33 2009 +0200
@@ -318,6 +318,7 @@
edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
commit
case c: Command =>
+ actor{Isabelle.plugin.command_change.event(c)}
if(current_document().commands.contains(c))
Swing_Thread.later {
// repaint if buffer is active
@@ -327,6 +328,8 @@
phase_overview.repaint()
}
}
+ case d: ProofDocument =>
+ actor{Isabelle.plugin.document_change.event(d)}
case x => System.err.println("warning: change_receiver ignored " + x)
}
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Thu Aug 27 12:12:11 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Aug 27 16:41:33 2009 +0200
@@ -147,6 +147,7 @@
val state = new Command_State(cmd)
states(state_id) = state
doc.states += (cmd -> state)
+ cmd.changed()
}
}
@@ -179,6 +180,7 @@
val (doc, structure_change) = old.text_changed(change)
document_versions ::= doc
edit_document(old, doc, structure_change)
+ change_receiver ! doc
}
case x => System.err.println("warning: ignored " + x)
}