src/Tools/jEdit/src/jedit/plugin.scala
changeset 39515 57ceabb0bb8e
parent 39241 e9a442606db3
child 39517 e036c67448e6
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 17 22:42:07 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 18 14:28:42 2010 +0200
     1.3 @@ -170,6 +170,12 @@
     1.4  
     1.5    private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
     1.6  
     1.7 +  def docked_session(view: View): Option[Session_Dockable] =
     1.8 +    wm(view).getDockableWindow("isabelle-session") match {
     1.9 +      case dockable: Session_Dockable => Some(dockable)
    1.10 +      case _ => None
    1.11 +    }
    1.12 +
    1.13    def docked_output(view: View): Option[Output_Dockable] =
    1.14      wm(view).getDockableWindow("isabelle-output") match {
    1.15        case dockable: Output_Dockable => Some(dockable)