Save terms in docstrings

Now, when elaborating definitions, terms included in `code blocks` in
docstrings are elaborated in the context that results from the
definition that they document. This means that they get semantic
coloring at the REPL, and IDEs can provide features like showing
implicits and further definition chasing.