diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean index fba7da5239..4974d39b88 100644 --- a/src/Lean/Elab/DocString.lean +++ b/src/Lean/Elab/DocString.lean @@ -1491,6 +1491,7 @@ private def elabModSnippet' logErrorAt b m!"Incorrect header nesting: expected at most `{"#".pushn '#' maxLevel}` \ but got `{"#".pushn '#' n}`" else + maxLevel := n + 1 let title ← liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := b}) <| name.mapM elabInline diff --git a/tests/lean/run/versoDocMarkdown.lean b/tests/lean/run/versoDocMarkdown.lean index 9d7e5bcf42..893759e415 100644 --- a/tests/lean/run/versoDocMarkdown.lean +++ b/tests/lean/run/versoDocMarkdown.lean @@ -8,6 +8,9 @@ set_option doc.verso true This module tests the Markdown rendering of all the builtin Verso docstring operators. Each section begins with a command that will fail when a new, untested operator is added. + +## Helpers + -/ section diff --git a/tests/lean/run/versoDocNesting.lean b/tests/lean/run/versoDocNesting.lean new file mode 100644 index 0000000000..333cff9d23 --- /dev/null +++ b/tests/lean/run/versoDocNesting.lean @@ -0,0 +1,58 @@ +set_option doc.verso true + +/-! +This test checks that header nesting rules are enforced within and across Verso module docs. + +First, within. + +# A +## B +### C +-/ + + +/-- error: Incorrect header nesting: expected at most `###` but got `####` -/ +#guard_msgs in +/-! +# A +## B +#### C +-/ + +/-- error: Incorrect header nesting: expected at most `##` but got `###` -/ +#guard_msgs in +/-! +# A +## B +### C +#### D +# E +### F +-/ + +/-! +Now, check between blocks. + +# A +## B +-/ + +/-! +### C +-/ + +/-- error: Incorrect header nesting: expected at most `####` but got `#####` -/ +#guard_msgs in +/-! +##### D +-/ + +/-! +# A +-/ + +/-- error: Incorrect header nesting: expected at most `##` but got `#####` -/ +#guard_msgs in +/-! +##### B +-/