include actions for jEdit dockables, e.g. "vfs.browser";
authorwenzelm
Tue, 03 Mar 2020 19:53:14 +0100
changeset 71514 61882acca79b
parent 71513 a403942212f2
child 71515 ce1222e9451e
include actions for jEdit dockables, e.g. "vfs.browser";
src/Pure/Tools/jedit.ML
--- 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;