equal
deleted
inserted
replaced
12 |
12 |
13 import scala.collection.mutable |
13 import scala.collection.mutable |
14 |
14 |
15 import org.gjt.sp.jedit.Buffer |
15 import org.gjt.sp.jedit.Buffer |
16 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} |
16 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} |
17 import org.gjt.sp.jedit.textarea.TextArea |
|
18 |
|
19 import java.awt.font.TextAttribute |
|
20 |
17 |
21 |
18 |
22 object Document_Model |
19 object Document_Model |
23 { |
20 { |
24 /* document model of buffer */ |
21 /* document model of buffer */ |