164 (case Properties.get props "NAME" of |
164 (case Properties.get props "NAME" of |
165 SOME name => if a = b then [name] else [] |
165 SOME name => if a = b then [name] else [] |
166 | NONE => []) |
166 | NONE => []) |
167 | parse_named _ _ = []; |
167 | parse_named _ _ = []; |
168 |
168 |
169 val jedit_actions = |
169 val isabelle_jedit_actions = |
170 (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of |
170 (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of |
171 XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
171 XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
172 | _ => []); |
172 | _ => []); |
173 |
173 |
174 val jedit_dockables = |
174 val isabelle_jedit_dockables = |
175 (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of |
175 (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of |
176 XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body |
176 XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body |
177 | _ => []); |
177 | _ => []); |
178 |
178 |
179 val all_actions = jedit_actions @ jedit_dockables; |
179 val jedit_actions = |
|
180 Lazy.lazy (fn () => |
|
181 (case Isabelle_System.bash_output |
|
182 "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of |
|
183 (txt, 0) => |
|
184 (case XML.parse txt of |
|
185 XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
|
186 | _ => []) |
|
187 | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc))); |
180 |
188 |
181 in |
189 in |
182 |
190 |
183 val is_action = member (op =) all_actions; |
191 fun is_action a = |
|
192 member (op =) isabelle_jedit_actions a orelse |
|
193 member (op =) isabelle_jedit_dockables a orelse |
|
194 member (op =) (Lazy.force jedit_actions) a; |
184 |
195 |
185 end; |
196 end; |
186 |
197 |
187 |
198 |
188 (* Isabelle/Isar entities (with index) *) |
199 (* Isabelle/Isar entities (with index) *) |