author | wenzelm |
Wed, 22 Oct 2014 17:30:58 +0200 | |
changeset 58766 | 5bab56d3dcd4 |
parent 58763 | 1b943a82d5ed |
child 58767 | 30766b5fd0e1 |
--- 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}