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