# HG changeset patch
# User wenzelm
# Date 1413991858 -7200
# Node ID 5bab56d3dcd4f002b800221583e15a4bdc37cc18
# Parent  1b943a82d5ed132fafb5ca9ab9e8135da6e31168
tuned imports;

diff -r 1b943a82d5ed -r 5bab56d3dcd4 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}