Commit 5f7c1de
authored
fix: skip only spaces at line start in Verso docstrings (#14191)
This PR fixes an issue where escaped content at the start of a line in a
valid block-opening positon in Verso content was skipped as if it were
whitespace.1 parent 9d518d9 commit 5f7c1de
12 files changed
Lines changed: 75 additions & 3 deletions
File tree
- src/Lean/DocString
- tests
- docparse
- elab
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
100 | 100 | | |
101 | 101 | | |
102 | 102 | | |
103 | | - | |
104 | | - | |
105 | 103 | | |
106 | 104 | | |
107 | 105 | | |
| |||
382 | 380 | | |
383 | 381 | | |
384 | 382 | | |
385 | | - | |
| 383 | + | |
386 | 384 | | |
387 | 385 | | |
388 | 386 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
0 commit comments