# HG changeset patch
# User wenzelm
# Date 1356982203 -3600
# Node ID 57abb2a814ab130ce8d1c6fe3f6bdc9be90dec31
# Parent  561d79d7031f7b6ffdbc868a58d1e1549d4353e9
tuned imports;

diff -r 561d79d7031f -r 57abb2a814ab src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Dec 31 16:56:54 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Dec 31 20:30:03 2012 +0100
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Window, Color, Point, Toolkit}
+import java.awt.{Graphics2D, Shape, Color, Point, Toolkit}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import java.awt.font.TextAttribute