--- a/src/Tools/jEdit/src/jedit/plugin.scala Fri Sep 17 22:42:07 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Sat Sep 18 14:28:42 2010 +0200
@@ -170,6 +170,12 @@
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
+ def docked_session(view: View): Option[Session_Dockable] =
+ wm(view).getDockableWindow("isabelle-session") match {
+ case dockable: Session_Dockable => Some(dockable)
+ case _ => None
+ }
+
def docked_output(view: View): Option[Output_Dockable] =
wm(view).getDockableWindow("isabelle-output") match {
case dockable: Output_Dockable => Some(dockable)