--- a/src/Pure/Tools/jedit.ML Tue Nov 10 21:52:18 2015 +0100
+++ b/src/Pure/Tools/jedit.ML Tue Nov 10 22:20:46 2015 +0100
@@ -44,16 +44,27 @@
| _ => [])
| (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
-fun is_action a =
- member (op =) (Lazy.force isabelle_jedit_actions) a orelse
- member (op =) (Lazy.force isabelle_jedit_dockables) a orelse
- member (op =) (Lazy.force jedit_actions) a;
+val all_actions =
+ Lazy.lazy (fn () =>
+ Lazy.force isabelle_jedit_actions @
+ Lazy.force isabelle_jedit_dockables @
+ Lazy.force jedit_actions);
in
-fun check_action (a, pos) =
- if is_action a then a
- else error ("Bad jEdit action " ^ quote a ^ Position.here pos);
+fun check_action (name, pos) =
+ if member (op =) (Lazy.force all_actions) name then name
+ else
+ let
+ val completion =
+ Completion.make (name, pos)
+ (fn completed =>
+ Lazy.force all_actions
+ |> filter completed
+ |> sort_strings
+ |> map (fn a => (a, ("action", a))));
+ val report = Markup.markup_report (Completion.reported_text completion);
+ in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
end;