> I guess the general question is, whether it is fine to add the plugin > infrastructure for (most of the) existing commands (e.g., definition, > typedef, record, fun), thus enabling us writing tools that extend the > command’s functionality (be them enabled by default or not). I am enthusiastically in favour of this proposal. Lars