tuned imports;
authorwenzelm
Mon, 31 Dec 2012 20:30:03 +0100
changeset 50657 57abb2a814ab
parent 50656 561d79d7031f
child 50658 0464c2007a25
tuned imports;
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