perf: reuse the file map when parsing code in docstrings This PR makes elaborating code in docstrings reuse the `FileMap` of the file instead of rebuilding it, and normalizing the line endings of the whole file again, for each code element. This made elaborating docstring-heavy files slower in proportion to their size times the number of such elements. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.