--- a/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 10:51:09 2009 +0200
@@ -135,30 +135,13 @@
msg match {
case epu: EditPaneUpdate => epu.getWhat match {
case EditPaneUpdate.BUFFER_CHANGED =>
- mapping get epu.getEditPane.getBuffer match {
- // only activate 'isabelle' buffers
- case None =>
- case Some(prover_setup) =>
- prover_setup.theory_view.activate
- val dockable =
- epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
- if (dockable != null) {
- val output_dockable = dockable.asInstanceOf[OutputDockable]
- if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
- output_dockable.asInstanceOf[OutputDockable].removeAll
- output_dockable.asInstanceOf[OutputDockable].
- add(new JScrollPane(prover_setup.output_text_view))
- output_dockable.revalidate
- }
- }
- }
+ val buffer = epu.getEditPane.getBuffer
+ (mapping get buffer) map (_.theory_view.activate)
+ buffer.propertiesChanged()
case EditPaneUpdate.BUFFER_CHANGING =>
val buffer = epu.getEditPane.getBuffer
- if (buffer != null) mapping get buffer match {
- // only deactivate 'isabelle' buffers
- case None =>
- case Some(prover_setup) => prover_setup.theory_view.deactivate
- }
+ if (buffer != null)
+ (mapping get buffer) map (_.theory_view.deactivate)
case _ =>
}
case _ =>
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Aug 27 10:51:09 2009 +0200
@@ -33,6 +33,7 @@
val buffer = view.getBuffer
theory_view = new TheoryView(view.getTextArea, prover)
+ theory_view.activate()
prover.set_document(theory_view.change_receiver, buffer.getName)
// register output-view
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200
@@ -79,9 +79,6 @@
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
buffer.addBufferListener(this)
-
- edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
- commit
}
def deactivate() {
@@ -102,7 +99,8 @@
loop {
react {
case ProverEvents.Activate =>
- activate()
+ edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
+ commit
case c: Command =>
update_delay()
repaint_delay()