| changeset 54441 | 3d37b2957a3e |
| parent 54325 | 2c4155003352 |
| child 54461 | 6c360a6ade0e |
--- a/src/Tools/jEdit/src/document_model.scala Thu Nov 14 17:17:57 2013 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Thu Nov 14 17:39:32 2013 +0100 @@ -14,9 +14,6 @@ import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} -import org.gjt.sp.jedit.textarea.TextArea - -import java.awt.font.TextAttribute object Document_Model