--- a/src/Tools/jEdit/src/rich_text_area.scala Sun Dec 13 13:46:28 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Dec 13 14:58:14 2020 +0100
@@ -16,13 +16,12 @@
import java.awt.font.TextAttribute
import javax.swing.SwingUtilities
import java.text.AttributedString
-import java.util.ArrayList
import scala.util.matching.Regex
import org.gjt.sp.util.Log
-import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
-import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.syntax.Chunk
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}