# HG changeset patch
# User wenzelm
# Date 1730560926 -3600
# Node ID f870d42c49463565489ae6c655cd4a7e756a7697
# Parent  177e6bb67e90dc479e2e84c2d37482723fafd4fb
tuned imports;

diff -r 177e6bb67e90 -r f870d42c4946 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 16:11:02 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 16:22:06 2024 +0100
@@ -9,16 +9,14 @@
 
 import isabelle._
 
-import java.awt.{BorderLayout, Dimension}
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
-  MouseEvent, MouseAdapter}
+import java.awt.BorderLayout
+import java.awt.event.KeyEvent
 import javax.swing.{JTree, JMenuItem}
-import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
-import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
+import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.event.TreeSelectionEvent
 
 import scala.collection.immutable.SortedMap
-import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation, BorderPanel}
-import scala.swing.event.ButtonClicked
+import scala.swing.{Button, Label, Component}
 
 import org.gjt.sp.jedit.{jEdit, View}
 import org.gjt.sp.jedit.menu.EnhancedMenuItem
diff -r 177e6bb67e90 -r f870d42c4946 src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 16:11:02 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 16:22:06 2024 +0100
@@ -9,20 +9,17 @@
 
 import isabelle._
 
-import java.awt.{BorderLayout, Dimension}
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
+import java.awt.Dimension
+import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
-import javax.swing.{JTree, JMenuItem, JComponent}
+import javax.swing.{JTree, JComponent}
 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
-import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
+import javax.swing.event.TreeSelectionEvent
 
-import scala.collection.immutable.SortedMap
-import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation, BorderPanel}
+import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
 import scala.swing.event.ButtonClicked
 
-import org.gjt.sp.jedit.{jEdit, View}
-import org.gjt.sp.jedit.menu.EnhancedMenuItem
-import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.View
 
 
 class Tree_Text_Area(view: View, root_name: String = "Overview") {