[Agda] .lagda.md in emacs interactive mode

[Martin Escardo]

Thanks, both.

What I am doing instead (for writing lecture notes) is:

* I have a file x.lagda (rather than x.lagda.md).

   This allows me to have holes. The code goes within \begin{code} and 
\end{code} environments, the rest is markdown of github flavour.

* To render it, I do `agda --html --html-highlight=code x.lagda`.

* This generates a file `html/x.tex` (which actually is not latex but 
instead text with html for the Agda code and the markdown code 
untouched) which I rename to `x.md` and then convert to html with some 
markdown processor.

This is done in a script, of course, and there are multiple files, not 
just `x`.

Because anyway if we had x.lagda.md we would still need to run `agda 
--html`, the above doesn't create extra steps other than renaming the 
.tex file to .md, but this is anyway in the same script that runs `agda 
--html`.

This needs the development version of Agda for the option 
`html-highlight=code`

Martin

On 11/03/2019 22:14, pedagand at gmail.com wrote:
>> On 11/03/2019 13.39, Martin Escardo wrote:
>>> When I start emacs with such a file, it doesn't start with the agda
>>> mode. Do I need to add something to my .emacs?
>>
>> The Emacs mode currently does not support .lagda.md files:
>>
>>     https://github.com/agda/agda/issues/2837
> 
> But that shouldn't stop you from trying: here is a .dir-locals
> 
> https://github.com/pedagand/MPRI-2.4-DTP/blob/master/.dir-locals.el
> 
> to put at the root at your project. Then, Emacs will let you load,
> edit, etc. your literate files.
> 
> For instance, this example (and all the others in that repos)
> 
> https://github.com/pedagand/MPRI-2.4-DTP/blob/master/01-effectful/Monad.lagda.rst
> 
> works like a charm (I use 'rst' files, YMMV with markdown).
> 
> 
> Use at your own risk,
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe