# HG changeset patch # User immler@in.tum.de # Date 1242992615 -7200 # Node ID 28fa2f219f01c49c8c16d265819dc5f8402f28aa # Parent d86023e76d3f786d27a9f884fcb7fc1a537bc324 fixed duplicate activation diff -r d86023e76d3f -r 28fa2f219f01 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.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()) diff -r d86023e76d3f -r 28fa2f219f01 src/Tools/jEdit/src/jedit/ProverSetup.scala --- 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 => diff -r d86023e76d3f -r 28fa2f219f01 src/Tools/jEdit/src/jedit/TheoryView.scala --- 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() = {