Bug in docstring code block error detection

edit: I did the tests below in 3.4.2, the behavior in 3.5.1 is detailed in the following comment.

I think the following is an accurate description of the current state of affairs: inside a docstring, adding a language tag to a code block surrounded by triple-backticks leads to an error if there's any non-whitespace text after the final code block.

A few examples:

No error:

/-!
```lean
code
```
-/

This gives the error invalid doc string, end of code block ``` expected (but it shouldn't):

/-!
```lean
code
```
non-whitespace text afterwards
-/

This gives no error:

/-!
```
code
```
non-whitespace text afterwards
-/

This example also gives no error. Compare this example in mathlib's reassoc_tactic) (pointed out by @robertylewis):

/-!
```lean
code
```
non-whitespace text afterwards
```
more code
```
-/

This gives an error (but it shouldn't):

/-!
```lean
code
```
non-whitespace text afterwards
```
more code
```
more non-whitespace text
-/

Lean thinks this is OK, but it isn't:

/-!
```lean
code
```
non-whitespace text afterwards
```
-/

The error message comes from src/library/documentation.cpp.

Originally reported by @jcommelin on zulip.

Start in src/library/documentation.cpp at the error reported around line 160, then reproduce the tagged and untagged code-block examples from the issue. Done means docstrings with a language-tagged triple-backtick block accept trailing non-whitespace text consistently with the examples and no longer emit the incorrect end-of-code-block error.