feat: make loose docstrings into elaboration errors rather than parse errors

[kmill]

Now loose docstrings will not yield a confusing parser error and instead log an "unexpected docstring" elaboration error and continue processing.

Furthermore, if the docstring is preceding the in command combinator, it will add a hint to the error:

unexpected doc string

Hint: the docstring must come after '... in', immediately before the declaration that accepts a docstring.

Closes #3135

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30a52b794a39256361050c52fe0e41bbff91bc8d --onto dd6ed124baef64a26ef5860f49597fdcef371239. (2024-08-09 17:43:40)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30a52b794a39256361050c52fe0e41bbff91bc8d --onto 5f31e938c1bf5bb2d6d2d29b26ea932ade115357. (2024-08-12 18:18:41)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e5e577865fe74ad17182346a225f8f209fa6e2e4 --onto 3ec55d3d498ce361f5886afee516d16df5cbd6fc. (2024-09-07 21:36:32)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit f1bb524.
There were significant changes against commit 30a52b7:

  Benchmark   Metric                 Change
  ====================================================
- parser      instructions             6.3% (6414.6 σ)
+ stdlib      fix level params        -1.8%  (-13.9 σ)
- stdlib      instantiate metavars     1.6%   (38.9 σ)

[kmill]

!bench

[leanprover-bot]

Here are the benchmark results for commit bd4c12d.
There were significant changes against commit e5e5778:

  Benchmark       Metric          Change
  ==================================================
- bv_decide_mul   branch-misses     2.6%    (13.5 σ)
- import Lean     task-clock       14.1%    (22.2 σ)
- import Lean     wall-clock       14.1%    (22.2 σ)
- parser          instructions      6.3% (15429.4 σ)