| changeset 66591 | 6efa351190d0 |
| parent 66206 | 2d2082db735a |
| child 67130 | b023f64e0d16 |
--- a/src/Tools/jEdit/src/symbols_dockable.scala Fri Sep 01 14:58:19 2017 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Sep 01 15:15:29 2017 +0200 @@ -8,6 +8,7 @@ import isabelle._ +import isabelle.jedit_base.Dockable import scala.swing.event.{SelectionChanged, ValueChanged} import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,