equal
deleted
inserted
replaced
76 |> map (fn a => (a, ("action", a)))); |
76 |> map (fn a => (a, ("action", a)))); |
77 in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ completion_report) end; |
77 in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ completion_report) end; |
78 |
78 |
79 val _ = |
79 val _ = |
80 Theory.setup |
80 Theory.setup |
81 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position) |
81 (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position) |
82 (fn ctxt => fn (name, pos) => |
82 (fn ctxt => fn (name, pos) => |
83 let |
83 let |
84 val _ = |
84 val _ = |
85 if Context_Position.is_reported ctxt pos |
85 if Context_Position.is_reported ctxt pos |
86 then ignore (check_action (name, pos)) |
86 then ignore (check_action (name, pos)) |