This PR sets the grammar scope for literate Agda to be text.tex.latex.agda, includes the text.tex.latex grammar and then only uses source.agda in code and verbatim blocks. This is in line with how language-haskell and language-knitr function, plus it makes the key bindings for latex function correctly.
banacorn
commented
7 years ago
This PR sets the grammar scope for literate Agda to be
text.tex.latex.agda, includes thetext.tex.latexgrammar and then only usessource.agdain code and verbatim blocks. This is in line with how language-haskell and language-knitr function, plus it makes the key bindings for latex function correctly.