--- a/src/Pure/Tools/jedit.ML Tue Mar 03 19:48:51 2020 +0100
+++ b/src/Pure/Tools/jedit.ML Tue Mar 03 19:53:14 2020 +0100
@@ -48,7 +48,8 @@
Lazy.lazy (fn () =>
(parse_actions (xml_file \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) @
parse_dockables (xml_file \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) @
- parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml"))
+ parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml") @
+ parse_dockables (xml_resource "org/gjt/sp/jedit/dockables.xml"))
|> sort_strings);
fun get_actions () = Lazy.force lazy_actions;