# HG changeset patch
# User wenzelm
# Date 1484060630 -3600
# Node ID 778c64c1736314c2a40ed218e5f6568901dd492b
# Parent  eec7ffef0be65d196af6df43d266d4c38cae9dfb
tuned;

diff -r eec7ffef0be6 -r 778c64c17363 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Tue Jan 10 09:47:23 2017 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Jan 10 16:03:50 2017 +0100
@@ -9,9 +9,6 @@
 
 import isabelle._
 
-import scala.swing.Button
-import scala.swing.event.ButtonClicked
-
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}