agda/agda — pull request #15 by pepijnkokke (2014-09-26 21:51:40+00:00)
Title: Added options for literate code in Bird-style and Markdown-style to Agda.

The behaviour of Agda was changed in the following manner:

* if the filename ends in "lagda" or "tex", the file will be processed using the rules for LaTeX-style literate code (which preserves backwards compatibility with the previous literate style);
* if the filename ends in "markdown" or "md", the file will be processed using the rules for Markdown-style literate code (which interprets any code in Bird tags and fenced code blocks as Agda source---we're currently not using the option of `unlit` to only use code blocks which are *marked* as containing Agda source);
* if the filename ends in "bird" the file is interpreted using the rules for Bird-style only;

The changes were implemented as follows:

* a new parser flag was introduced (parseCodeStyle) which can take one of the following values: CSCode, CSLaTeX, CSMarkdown or CSBird;
* this flag is set based on the file extension in `Parser.hs`---I wasn't sure that parseLiterateFile and parseFile weren't called from elsewhere, so I changed the code such that if *any* exported function is called it should work;
* in the file `Monad.hs` the external function Unlit.unlit is called with the appropriate configuration.

What I haven't done:

* I have made no attempt at removing the previous literate code mechanism, since it seems to be entwined in the lexer code (and I don't want to introduce errors in that);