more derived actions, according to jEdit/org/gjt/sp/jedit/gui/DockableWindowFactory.java;
authorwenzelm
Sat Sep 16 17:25:51 2017 +0200 (21 months ago)
changeset 66670e5188cb1c3d8
parent 66669 bbcb75c58086
child 66671 41b64e53b6a1
more derived actions, according to jEdit/org/gjt/sp/jedit/gui/DockableWindowFactory.java;
src/Pure/Tools/jedit.ML
     1.1 --- a/src/Pure/Tools/jedit.ML	Sat Sep 16 16:19:34 2017 +0200
     1.2 +++ b/src/Pure/Tools/jedit.ML	Sat Sep 16 17:25:51 2017 +0200
     1.3 @@ -32,7 +32,8 @@
     1.4    Lazy.lazy (fn () =>
     1.5      (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
     1.6        XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
     1.7 -    | _ => []));
     1.8 +    | _ => [])
     1.9 +    |> maps (fn a => [a, a ^ "-toggle", a ^ "-float"]));
    1.10  
    1.11  val jedit_actions =
    1.12    Lazy.lazy (fn () =>