Handle footnotes

[pbelmans]

This is important, and right now not taken care of at all. I hope it won't be too hard...

[PatrickMassot]

What do you mean by "not taken care of at all"? The command footnote exists and XHTML and HTML5 renderers have corresponding templates see Footnotes.jinja2s for the main text mark and how the note text appears in the default layout.

[pbelmans]

PlasTeX indeed has the functionality to deal with them, we just don't deal with them at the moment. We need footnotes to appear whenever they are used: if within a section 2 lemmas use a footnote, we need a footnote in the output for each each lemma, and both footnotes in the section output file.

Possible issues are:

• we need to number footnotes depending on the context, as a single footnote might need to receive multiple numbers
• what if both the statement and the proof contain a footnote? this is related to the previous issue

[pbelmans]

One possible solution is to write each footnote to a file, like we do for all tags and proofs anyway. Then based on the HTML output it is possible to link footnotes to tags and proofs. This is not very clean, maybe there is a cleaner way of exporting this to a file called footnotes which links their id's to filenames where they appear, but I don't see a way to do this, yet.

[pbelmans]

I've been experimenting a little.

One not entirely correct solution would be to wrap all footnotes where they appear in an <aside>, exactly where they are used. In CSS we'd just hide these, as footnotes are not supposed to be important anyway, and we let JavaScript collect all footnotes on a page and display them on the bottom, and at the same time fix the numbering.

In an ideal world I would just write all footnotes to their own files, and let gerby-tools look for links to footnotes. Then we could assign footnotes to tags, but then we'd end up dealing with footnotes appearing in proofs versus footnotes in statements, etc. etc. Also, this wouldn't give the correct numbering.

The JavaScript solution seems to be the most flexible to be honest. Or, we could do this in Flask to make sure the HTML output is good as it is. But a plasTeX solution doesn't seem feasible.

[chngr]

Another, perhaps equally spotty solution, would be to render the footnotes where they appear, then use the postProcess argument in the cleanup process at the end of rendering to extract out the rendered footnotes.

Something that I have been trying to get work is just simply extract out a rendered form of the footnotes at the end of the rendering process. You can do this at the end of the render method by looking at document.userdata["footnotes"]; each footnote element is stored there by the end of the rendering process. However, I have been unable to figure out how to get plasTeX to process the raw TeXFragment and give me a rendered string.

[pbelmans]

This was implemented in #17. Its output looked good, I'm now implementing things in the website, then we'll see if there are things we have forgotten about.