equal
deleted
inserted
replaced
38 val lazy_actions = |
38 val lazy_actions = |
39 Lazy.lazy (fn () => |
39 Lazy.lazy (fn () => |
40 (parse_resources o map File.read) |
40 (parse_resources o map File.read) |
41 [\<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>, |
41 [\<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>, |
42 \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>] @ |
42 \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>] @ |
43 (parse_resources o \<^scala>\<open>jEdit.resources\<close>) ["actions.xml", "dockables.xml"] |
43 (parse_resources o \<^scala>\<open>jEdit.resource\<close>) ["actions.xml", "dockables.xml"] |
44 |> sort_strings); |
44 |> sort_strings); |
45 |
45 |
46 fun get_actions () = Lazy.force lazy_actions; |
46 fun get_actions () = Lazy.force lazy_actions; |
47 |
47 |
48 fun check_action (name, pos) = |
48 fun check_action (name, pos) = |