more thorough check_action, including completion;

--- a/src/Doc/antiquote_setup.ML	Tue Nov 10 21:52:18 2015 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Nov 10 22:20:46 2015 +0100
@@ -166,8 +166,6 @@
     | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
   end;
 
-fun check_action _ = can JEdit.check_action;
-
 val arg = enclose "{" "}" o clean_string;
 
 fun entity check markup binding index =
@@ -222,7 +220,7 @@
     entity_antiqs no_check "isasystem" @{binding executable} #>
     entity_antiqs check_tool "isatool" @{binding tool} #>
     entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
-    entity_antiqs check_action "isasystem" @{binding action});
+    entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
 
 end;
 

--- 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;