fixed duplicate activation
authorimmler@in.tum.de
Fri, 22 May 2009 13:43:35 +0200
changeset 34566 28fa2f219f01
parent 34565 d86023e76d3f
child 34567 d9e4b940cf7e
fixed duplicate activation
src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
src/Tools/jEdit/src/jedit/ProverSetup.scala
src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Fri May 22 13:43:35 2009 +0200
@@ -18,11 +18,12 @@
 import org.gjt.sp.jedit.buffer.JEditBuffer;
 import org.gjt.sp.jedit._
 
-class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: (String, Int) => Int) extends JPanel(new BorderLayout) {
+class PhaseOverviewPanel(prover: isabelle.prover.Prover,
+                         textarea: JEditTextArea,
+                         to_current: (String, Int) => Int) extends JPanel(new BorderLayout) {
 
   private val WIDTH = 10
 	private val HILITE_HEIGHT = 2
-  var textarea : JEditTextArea = null
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
 
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Fri May 22 13:43:35 2009 +0200
@@ -42,6 +42,7 @@
     prover.set_document(theory_view.change_receiver,
       if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path)
     theory_view.activate
+    prover ! new isabelle.proofdocument.Text.Change(Isabelle.plugin.id(), 0,buffer.getText(0, buffer.getLength),0)
 
     //register output-view
     prover.output_info += (text =>
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
@@ -59,7 +59,7 @@
   col_timer.setRepeats(true)
 
 
-  private val phase_overview = new PhaseOverviewPanel(prover, to_current)
+  private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current)
 
 
   /* activation */
@@ -76,11 +76,9 @@
 
   def activate() = {
     text_area.addCaretListener(selected_state_controller)
-    phase_overview.textarea = text_area
     text_area.addLeftOfScrollBar(phase_overview)
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
-    document_actor ! new Text.Change(id(), 0,buffer.getText(0, buffer.getLength),0)
   }
 
   def deactivate() = {