changeset 66591 | 6efa351190d0 |
parent 66206 | 2d2082db735a |
child 71704 | b9a5eb0f3b43 |
--- a/src/Tools/jEdit/src/info_dockable.scala Fri Sep 01 14:58:19 2017 +0200 +++ b/src/Tools/jEdit/src/info_dockable.scala Fri Sep 01 15:15:29 2017 +0200 @@ -8,6 +8,7 @@ import isabelle._ +import isabelle.jedit_base.Dockable import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}