src/Tools/jEdit/src/query_dockable.scala

--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Aug 27 12:51:57 2020 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu Aug 27 13:06:58 2020 +0200
@@ -215,10 +215,8 @@
         }
 
       _items =
-        Print_Operation.print_operations(PIDE.session).map(
-          {
-            case (name, description) => new Item(name, description, was_selected(name))
-          })
+        for ((name, description) <- Print_Operation.get(PIDE.session))
+        yield new Item(name, description, was_selected(name))
       _items
     }