argumentcomputer / Megaparsec.lean

Lean 4 port of Megaparsec

MIT License

22 stars 4 forks source link

Usability: Errors in bundles should be sorted by offset #18

Open cognivore opened 2 years ago

cognivore commented 2 years ago

Why?

Currently, we don't guarantee the order in error bundles (see runParserT'), That's poor UX because the author of a parser would like to see errors from left to right, in order of appearance.

How?

[ ] Implement sorting on NonEmptyLists
[ ] Use it in runParserT' and wherever else we build bundles
[x] Perhaps, make a function that makes bundles in Bundle.lean (!)

cognivore commented 2 years ago

Related: #14

ixahedron commented 2 years ago

Can you provide an example of this behaviour (where errors end up in the wrong order)?