Cornelis not loading properly for .lagda.md files

[aricursion]

Hi! I"m having an issue specifically with .lagda.md files. Whenever I try to load them, my neovim just recognizes them as regular markdown files. Because of this, I can't seem to call CornelisLoad or any other related functions. Does anyone know how I can make this work?

My Agda version is 2.6.2.2 (the default when installed with stack) and my stack install is managed with ghcup

Thanks so much!!

~~unrelated, I'm having a minor issue that whenever I open a regular .agda file it prompts me with all possible keybinds before letting me edit the file. Is this intended?~~

[isovector]

I ran into this too. The issue is that neovim's default file type detection also recognizes markdown files, and wins the conflict.

You can work around it by explicitly setting your file type via :setf agda

On Wed, Jul 6, 2022, 10:04 PM z @.***> wrote:

Hi! I"m having an issue specifically with .lagda.md files. Whenever I try to load them, my neovim just recognizes them as regular markdown files. Because of this, I can't seem to call CornelisLoad or any other related functions. Does anyone know how I can make this work? Thanks so much!!

unrelated, I'm having a minor issue that whenever I open a regular .agda file it prompts me with all possible keybinds before letting me edit the file. Is this intended?

— Reply to this email directly, view it on GitHub https://github.com/isovector/cornelis/issues/61, or unsubscribe https://github.com/notifications/unsubscribe-auth/AACLAFZ6CBTMPJKKSDH5RHLVSXKFBANCNFSM522YRONQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[chezbgone]

I automated this with

autocmd BufNewFile,BufRead *.lagda.md set filetype=agda

[Eloitor]

My configuration is written in lua and I didn't know where to place this. After reading https://neovim.io/doc/user/filetype.html I placed this in ~/.config/nvim/ftdetect/

It works well, but I wonder why "agda" does not appear in the status line... Edit2: After commenting line 788 of cornelis/agda-input.vim this works as expected ("agda apears in the status line")

By the way,

autocmd BufNewFile,BufRead *.lagda.md set filetype=agda.markdown

works better for me, it enables markdown's syntax highlighting.

Edit: After running CornelisLoad the syntax highlighting for markdown is lost... Edit2: By the way, after runing CornelisLoad and running :mes I get an error on line 788 of cornelis/agda-input.vim. This error caused E13 "file exists, add ! to override" every time I saved the file. Commenting line 788 solved the problem. Can someone try this too?

Steps to reproduce:

1. open the file https://github.com/martinescardo/HoTTEST-Summer-School/blob/main/Agda/Exercises/01-Exercises.lagda.md
2. :setf agda
3. :CornelisLoad
4. :mes

[isovector]

Should be fixed in the latest commit; I was using setf instead of setlocal filetype, which I thought were the same but are not in fact.