diff options
| author | Emilio Jesus Gallego Arias | 2018-10-18 23:19:50 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-29 23:35:47 +0200 |
| commit | 7eefc0b1db614158ed1b322f8c6e5601e3995113 (patch) | |
| tree | 44e1d73a5ce6337b2aceaa20d42781b57bc23219 /dev/include_printers | |
| parent | 69daead8ae18d55ee445a918865ea2adf59439eb (diff) | |
[stm] Add hooks for document actions.
This arose after a question by Talia Ringer on how to log
user-interaction with a Coq document.
The hooks would allow a plugin to receive events about user data.
This is experimental and will need some tweaks to be useful for sure,
in particular w.r.t. errors.
[Note: this is safe enough as to be included in 8.9]
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions