1.1 --- a/src/Doc/antiquote_setup.ML Tue Nov 10 21:52:18 2015 +0100
1.2 +++ b/src/Doc/antiquote_setup.ML Tue Nov 10 22:20:46 2015 +0100
1.3 @@ -166,8 +166,6 @@
1.4 | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
1.5 end;
1.6
1.7 -fun check_action _ = can JEdit.check_action;
1.8 -
1.9 val arg = enclose "{" "}" o clean_string;
1.10
1.11 fun entity check markup binding index =
1.12 @@ -222,7 +220,7 @@
1.13 entity_antiqs no_check "isasystem" @{binding executable} #>
1.14 entity_antiqs check_tool "isatool" @{binding tool} #>
1.15 entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
1.16 - entity_antiqs check_action "isasystem" @{binding action});
1.17 + entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
1.18
1.19 end;
1.20
2.1 --- a/src/Pure/Tools/jedit.ML Tue Nov 10 21:52:18 2015 +0100
2.2 +++ b/src/Pure/Tools/jedit.ML Tue Nov 10 22:20:46 2015 +0100
2.3 @@ -44,16 +44,27 @@
2.4 | _ => [])
2.5 | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
2.6
2.7 -fun is_action a =
2.8 - member (op =) (Lazy.force isabelle_jedit_actions) a orelse
2.9 - member (op =) (Lazy.force isabelle_jedit_dockables) a orelse
2.10 - member (op =) (Lazy.force jedit_actions) a;
2.11 +val all_actions =
2.12 + Lazy.lazy (fn () =>
2.13 + Lazy.force isabelle_jedit_actions @
2.14 + Lazy.force isabelle_jedit_dockables @
2.15 + Lazy.force jedit_actions);
2.16
2.17 in
2.18
2.19 -fun check_action (a, pos) =
2.20 - if is_action a then a
2.21 - else error ("Bad jEdit action " ^ quote a ^ Position.here pos);
2.22 +fun check_action (name, pos) =
2.23 + if member (op =) (Lazy.force all_actions) name then name
2.24 + else
2.25 + let
2.26 + val completion =
2.27 + Completion.make (name, pos)
2.28 + (fn completed =>
2.29 + Lazy.force all_actions
2.30 + |> filter completed
2.31 + |> sort_strings
2.32 + |> map (fn a => (a, ("action", a))));
2.33 + val report = Markup.markup_report (Completion.reported_text completion);
2.34 + in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
2.35
2.36 end;
2.37