| changeset 36015 | 6111de7c916a |
| parent 34871 | e596a0b71f3c |
| child 36760 | b82a698ef6c9 |
| 36014:c51a077680e4 | 36015:6111de7c916a |
|---|---|
5 * @author Makarius |
5 * @author Makarius |
6 */ |
6 */ |
7 |
7 |
8 package isabelle.jedit |
8 package isabelle.jedit |
9 |
9 |
10 |
|
11 import isabelle._ |
|
10 |
12 |
11 import scala.actors.Actor, Actor._ |
13 import scala.actors.Actor, Actor._ |
12 import scala.collection.mutable |
14 import scala.collection.mutable |
13 |
15 |
14 import org.gjt.sp.jedit.Buffer |
16 import org.gjt.sp.jedit.Buffer |