In CompCert, we allow a template for a diagnostic message to contain the special form $i, where i is an integer constant, understood as an index into the parser’s stack. The code in cparser/ErrorReports.ml automatically replaces this special form with the fragment of the source text that corresponds to this stack entry. This mechanism is not built into Menhir ; it is implemented in CompCert using Menhir’s incremental API.
It would be interesting to get some hooks for this behavior into Menhir directly. It can’t be completely seamless because different parsers will have different data structures for storing source text, but it could be made easy.