src/Doc/antiquote_setup.ML
changeset 61617 cd7549cd5fe7
parent 61616 abbecf4e6601
child 61618 27af754f50ca
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Nov 10 19:56:51 2015 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Nov 10 20:10:17 2015 +0100
     1.3 @@ -141,46 +141,6 @@
     1.4              #> enclose "\\isa{" "}")));
     1.5  
     1.6  
     1.7 -(* Isabelle/jEdit elements *)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun parse_named a (XML.Elem ((b, props), _)) =
    1.12 -      (case Properties.get props "NAME" of
    1.13 -        SOME name => if a = b then [name] else []
    1.14 -      | NONE => [])
    1.15 -  | parse_named _ _ = [];
    1.16 -
    1.17 -val isabelle_jedit_actions =
    1.18 -  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
    1.19 -    XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    1.20 -  | _ => []);
    1.21 -
    1.22 -val isabelle_jedit_dockables =
    1.23 -  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
    1.24 -    XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
    1.25 -  | _ => []);
    1.26 -
    1.27 -val jedit_actions =
    1.28 -  Lazy.lazy (fn () =>
    1.29 -    (case Isabelle_System.bash_output
    1.30 -      "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
    1.31 -      (txt, 0) =>
    1.32 -        (case XML.parse txt of
    1.33 -          XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    1.34 -        | _ => [])
    1.35 -    | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
    1.36 -
    1.37 -in
    1.38 -
    1.39 -fun is_action a =
    1.40 -  member (op =) isabelle_jedit_actions a orelse
    1.41 -  member (op =) isabelle_jedit_dockables a orelse
    1.42 -  member (op =) (Lazy.force jedit_actions) a;
    1.43 -
    1.44 -end;
    1.45 -
    1.46 -
    1.47  (* Isabelle/Isar entities (with index) *)
    1.48  
    1.49  local
    1.50 @@ -275,7 +235,7 @@
    1.51      entity_antiqs no_check "isasystem" @{binding executable} #>
    1.52      entity_antiqs check_tool "isatool" @{binding tool} #>
    1.53      entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
    1.54 -    entity_antiqs (K (is_action o #1)) "isasystem" @{binding action});
    1.55 +    entity_antiqs (K (JEdit.is_action o #1)) "isasystem" @{binding action});
    1.56  
    1.57  end;
    1.58