--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Aug 27 10:51:09 2009 +0200
@@ -30,7 +30,7 @@
val data = new SideKickParsedData(buffer.getName)
- val prover_setup = Isabelle.plugin.prover_setup(buffer)
+ val prover_setup = Isabelle.prover_setup(buffer)
if (prover_setup.isDefined) {
val document = prover_setup.get.theory_view.current_document()
for (command <- document.commands)
--- 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
@@ -96,6 +96,15 @@
}
+ /* 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) }
+
+
/* mapping buffer <-> prover */
private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
--- 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
@@ -24,12 +24,6 @@
var prover: Prover = null
var theory_view: TheoryView = null
- 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) }
-
val output_text_view = new JTextArea
def activate(view: View)
@@ -57,21 +51,6 @@
}
})
- // register for state-view
- state_update += (cmd => {
- val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
- val state_panel =
- if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
- else null
- if (state_panel != null) {
- if (cmd == null)
- state_panel.setDocument(null: Document)
- else
- state_panel.setDocument(cmd.result_document(theory_view.current_document()),
- UserAgent.base_URL)
- }
- })
-
}
def deactivate
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Thu Aug 27 10:51:09 2009 +0200
@@ -59,6 +59,15 @@
// scrolling
add(new FSScrollPane(panel), BorderLayout.CENTER)
+ // register for state-view
+ Isabelle.plugin.state_update += (cmd => {
+ val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
+ if (cmd == null)
+ panel.setDocument(null: org.w3c.dom.Document)
+ else
+ panel.setDocument(cmd.result_document(theory_view.current_document()),
+ UserAgent.base_URL)
+ })
private val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
--- 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
@@ -68,8 +68,8 @@
val doc = current_document()
val cmd = doc.find_command_at(e.getDot)
if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
- Isabelle.prover_setup(buffer).get.selected_state != cmd)
- Isabelle.prover_setup(buffer).get.selected_state = cmd
+ Isabelle.plugin.selected_state != cmd)
+ Isabelle.plugin.selected_state = cmd
}
}
@@ -130,8 +130,8 @@
val stop = text_area.getLineOfOffset(to_current(document, cmd.stop(document)) - 1)
text_area.invalidateLineRange(start, stop)
- if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
- Isabelle.prover_setup(buffer).get.selected_state = cmd // update State view
+ if (Isabelle.plugin.selected_state == cmd)
+ Isabelle.plugin.selected_state = cmd // update State view
}
}