Reed Mullanix
Reed Mullanix
I discussed the issue with the maintainers and it's a WONTFIX 😔 However, it looks like the emacs community has decided that https://github.com/joaotavora/eglot is the implementation of choice, and has...
So the 1lab uses `--no-load-primitives`, but there's an agda bug where it tries to get the primitive dir [here](https://github.com/agda/agda/blob/master/src/full/Agda/Compiler/Common.hs#L57), and crashes. This is blocked on that bug.
Should be fixed in https://github.com/agda/agda/pull/6161
FWIW, `dune pkg` also ignores `:with-dev-setup`.
I mostly chose the name for the sake of consistency; I suppose we could call it `prepend_rev` or `prepend_bwd` instead.
Sorry for incomplete match errors; I was using GHC `8.10.7` and didn't realize that the warning had been disabled for versions under 9.
Ugh, VSCode being a bad citizen yet again... As for the data structure, I think some sort of rope segmented at points where UTF-16 and UTF-8 offsets disagree ought to...
That's a reasonable ask! Just to confirm, this is only for Asai's diagnostic chrome, and not for unicode that appears in programmer supplied messages?
I think a pure ASCII backend is probably the move instead of offering per-character settings. I'll take a look at this later today
Rebased onto main, just need a ✅ and we are good to go.