# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 73727c7eec646799d127798685ea2d3419f29eda
# Parent  51e98c01cbd651ee3650678ef721c45ad152f027
state_update global in Plugin

diff -r 51e98c01cbd6 -r 73727c7eec64 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- 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)
diff -r 51e98c01cbd6 -r 73727c7eec64 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
@@ -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]
diff -r 51e98c01cbd6 -r 73727c7eec64 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
@@ -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
diff -r 51e98c01cbd6 -r 73727c7eec64 src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- 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]
diff -r 51e98c01cbd6 -r 73727c7eec64 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
@@ -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
     }
   }