# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID c99878d7bec70007a561f4cad0e1b727b52dcd1c
# Parent  73727c7eec646799d127798685ea2d3419f29eda
proper activation with multiple buffers

diff -r 73727c7eec64 -r c99878d7bec7 src/Tools/jEdit/src/jedit/Plugin.scala
--- 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 _ =>
diff -r 73727c7eec64 -r c99878d7bec7 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- 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
diff -r 73727c7eec64 -r c99878d7bec7 src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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()