# HG changeset patch
# User wenzelm
# Date 1607867894 -3600
# Node ID 4e4b4298f1e7579b7830358c5ced21884f864253
# Parent  86eff7a823f3665bedf50ad0c400d6da0ca3929b
tuned imports;

diff -r 86eff7a823f3 -r 4e4b4298f1e7 src/Tools/jEdit/src/rich_text_area.scala
--- 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}