[Agda] Markdown and Agda

[Francesco Mazzoli]

At Tue, 2 Apr 2013 15:18:28 +0200,
Wojciech Jedynak wrote:
> 
> Hi Francesco,
> 
> This looks really useful - thanks for sharing!
> I guess that by metadata you mean the '\begin{code}' and '\end{code}' tags?
> If you want to make the non-agda code (like the part with 'undefined')
> stand out, maybe a different background color would suffice?
> 
> Greetings,
> Wojciech

Hi Wojciech,

(CCing the list back, might be of interest)

No, I mean the ‘title’ and ‘date’ things at the top of the page—usually Hakyll
uses and then discards them, but with my script they stay.

For what concerns \begin{code} and \end{code}, I’m still not sure what to make
of them.  I think it’s nice, even if only conceptually, to have something that
will work if you wanted to paste it in an editor.  OTOH it’s a bit redundant.
I’ll have to think more about it :).

Francesco