src/Tools/jEdit/src/pretty_text_area.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Oct 22 17:04:45 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Oct 22 17:30:58 2014 +0200
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
+import java.awt.{Color, Font, Toolkit, Window}
 import java.awt.event.KeyEvent
 import javax.swing.JTextField
 import javax.swing.event.{DocumentListener, DocumentEvent}