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.
87 lines
1.5 KiB
Text
87 lines
1.5 KiB
Text
import Lean
|
|
|
|
set_option doc.verso true
|
|
|
|
/-!
|
|
This test ensures that syntax errors in Verso docs are appropriately reported.
|
|
-/
|
|
|
|
-- Syntax error in module docstring should report actual error location
|
|
/--
|
|
error: '}'
|
|
---
|
|
error: unexpected end of input; expected '![', '$$', '$', '[' or '[^'
|
|
-/
|
|
#guard_msgs in
|
|
/-!
|
|
Here is text with an unclosed role {name`Nat
|
|
-/
|
|
|
|
-- Syntax error with specific position (not at end of docstring)
|
|
/--
|
|
@ +2:27...*
|
|
error: '*'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
Some mismatched *formatting_
|
|
|
|
A b c d e f.
|
|
|
|
```
|
|
-/
|
|
|
|
-- Syntax error in a normal docstring
|
|
/--
|
|
@ +2:27...*
|
|
error: '*'
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/--
|
|
Some mismatched *formatting_
|
|
|
|
A b c d e f.
|
|
-/
|
|
def x := 5
|
|
|
|
-- Unmatched closing bracket in docstring (issue #12118)
|
|
/--
|
|
@ +2:0...*
|
|
error: '{'; expected %%% (at line beginning), '![', '$$', '$', '[', '[^', *, + or -
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/--
|
|
}
|
|
-/
|
|
def z := 0
|
|
|
|
-- Unmatched closing bracket in module docstring
|
|
/--
|
|
@ +2:0...*
|
|
error: '{'; expected %%% (at line beginning), '![', '$$', '$', '[', '[^', *, + or -
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
}
|
|
-/
|
|
|
|
-- Unmatched closing square bracket in docstring
|
|
/--
|
|
@ +2:0...*
|
|
error: '{'; expected %%% (at line beginning), '![', '$$', '$', '[', '[^', *, + or -
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/--
|
|
]
|
|
-/
|
|
def w := 0
|
|
|
|
-- Unmatched closing square bracket in module docstring
|
|
/--
|
|
@ +2:0...*
|
|
error: '{'; expected %%% (at line beginning), '![', '$$', '$', '[', '[^', *, + or -
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
/-!
|
|
]
|
|
-/
|