| changeset 66591 | 6efa351190d0 |
| parent 66082 | 2d12a730a380 |
| child 71525 | d7b0d078266d |
--- a/src/Tools/jEdit/src/documentation_dockable.scala Fri Sep 01 14:58:19 2017 +0200 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Fri Sep 01 15:15:29 2017 +0200 @@ -8,6 +8,7 @@ import isabelle._ +import isabelle.jedit_base.Dockable import java.awt.Dimension import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}