0e19692d0b
This PR fixes poor error reporting from Verso docstrings. Before, if the Verso parser didn't consume the whole docstring, then Lean would try to parse the closing -/ and fail; this would lead to backtracking and an assumption that the docstring must be non-Verso, with only the non-Verso commands like #guard_msgs as possibilities. Now, the input is always consumed. Closes #12118. |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| CMakeLists.txt | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||