# HG changeset patch
# User wenzelm
# Date 1583261594 -3600
# Node ID 61882acca79b8d06efb5d9f84bc24f6dd423acf8
# Parent  a403942212f2bf5edfafb366e607e755264dcd52
include actions for jEdit dockables, e.g. "vfs.browser";

diff -r a403942212f2 -r 61882acca79b 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;