@@ -83,11 +83,21 @@
8383 as they were given in the source files.
8484+ Backslash, braces and percent symbols are now correctly pretty printed
8585 in LaTeX.
86−+ Parse errors have a new format, similar to GHC 8.2's default, due to a
87− switch from Trifecta to Megaparsec for parsing. This could possibly cause
88− some subtle deviations in parsing from previous versions of Idris.
89−+ Non-parse errors and warnings have mostly been converted to mimic the parse
90− error format.
86++ Errors and warnings now consistently have the following format:
87+ ```idris
88+ reg068.idr:1:6-8:
89+ |
90+ 1 | data nat : Type where --error
91+ | ~~~
92+ Main.nat has a name which may be implicitly bound.
93+ This is likely to lead to problems!
94+ ```
95+ The code is highlighted when highlighting information is available. How
96+ much highlighting information is available depends on where the error
97+ occurred.
98++ The parser provider has been switched from Trifecta to Megaparsec. This
99+ could possibly cause some subtle deviations in parsing from previous
100+ versions of Idris.
91101+ Many more errors now report beginning *and* ending position (which may be
92102 on different lines), instead of just a single point. The format is
93103 `Foo.idr:9:7-15:` if ending column is on the same line or