| changeset 36015 | 6111de7c916a |
| parent 34871 | e596a0b71f3c |
| child 36760 | b82a698ef6c9 |
--- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Mar 30 00:12:42 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Mar 30 00:13:27 2010 +0200 @@ -8,6 +8,8 @@ package isabelle.jedit +import isabelle._ + import scala.actors.Actor._ import java.awt.event.{MouseAdapter, MouseEvent}