De-indent comment block

[nomeata]

Browsing the documentation I was a bit confused why some paragraphs are randomly indendet, e.g. “The bvar constructor…”.

My theory is that it’s because the whole doc string block is indented in the source code:

/--
Lean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
-/
inductive Expr where
  /--
  The `bvar` constructor represents bound variables, i.e. occurrences
  of a variable in the expression where there is a variable binder
  above it (i.e. introduced by a `lam`, `forallE`, or `letE`).
  …
  -/
  | bvar (deBruijnIndex : Nat)

Looking at this, I doubt that the author wanted to have the markdown interpreted as indented.

If that analysis is correct, maybe the tool should de-indent by all common whitespace?

Probably also for

/--
  This style, which I have seen too.
-/
def foo := …

I might be barking on the wrong hill, though.

[hargoniX]

With respect to docstring rendering I'm currently hoping that David's new doc tooling will give some clear semantics to docstrings at last that the doc-gen renderer can then just stick to. Hence I'd suggest to hold our breaths for the first release of that.

[nomeata]

Fair enough, and the issue isn't servere.

[acmepjz]

I think this is a CSS problem...