src/Tools/jEdit/src-base/pide_docking_framework.scala
changeset 73909 1d0d9772fff0
parent 73340 0ffcad1f6130
--- a/src/Tools/jEdit/src-base/pide_docking_framework.scala	Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala	Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,7 @@
 
 import isabelle._
 
+import java.util.{List => JList}
 import java.awt.event.{ActionListener, ActionEvent}
 import javax.swing.{JPopupMenu, JMenuItem}
 
@@ -42,7 +43,7 @@
             }
 
           case panel: PanelWindowContainer =>
-            val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
+            val entries = Untyped.get[JList[AnyRef]](panel, "dockables").toArray
             val wins =
               (for {
                 entry <- entries.iterator