--- a/src/Doc/antiquote_setup.ML Tue Nov 10 19:56:51 2015 +0100
+++ b/src/Doc/antiquote_setup.ML Tue Nov 10 20:10:17 2015 +0100
@@ -141,46 +141,6 @@
#> enclose "\\isa{" "}")));
-(* Isabelle/jEdit elements *)
-
-local
-
-fun parse_named a (XML.Elem ((b, props), _)) =
- (case Properties.get props "NAME" of
- SOME name => if a = b then [name] else []
- | NONE => [])
- | parse_named _ _ = [];
-
-val isabelle_jedit_actions =
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
- XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
- | _ => []);
-
-val isabelle_jedit_dockables =
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
- XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
- | _ => []);
-
-val jedit_actions =
- Lazy.lazy (fn () =>
- (case Isabelle_System.bash_output
- "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
- (txt, 0) =>
- (case XML.parse txt of
- XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
- | _ => [])
- | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
-
-in
-
-fun is_action a =
- member (op =) isabelle_jedit_actions a orelse
- member (op =) isabelle_jedit_dockables a orelse
- member (op =) (Lazy.force jedit_actions) a;
-
-end;
-
-
(* Isabelle/Isar entities (with index) *)
local
@@ -275,7 +235,7 @@
entity_antiqs no_check "isasystem" @{binding executable} #>
entity_antiqs check_tool "isatool" @{binding tool} #>
entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
- entity_antiqs (K (is_action o #1)) "isasystem" @{binding action});
+ entity_antiqs (K (JEdit.is_action o #1)) "isasystem" @{binding action});
end;