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