Implement support for converting values to GIFs

[jackfirth]

Closes #231. This pull request only touches the HTML rendering implementation code; it has no tests and does not yet update the docs. I'd like to get some feedback on whether this is the right implementation approach before getting to tests and docs.

[jackfirth]

Manually tested this on my machine and it works. But I don't know how to write an automated test for this, or which places in the documentation need to be updated. Suggestions greatly appreciated!

[samth]

Looking at the existing tests, I don't see anything that tests any aspects of the html rendering.

A number of places (core.scrbl, running.scrbl) seem to mention the supported formats.

There's also the --convert flag, which should maybe also accept gif, and the render-convertible-as property. I don't know if it makes sense to change all these, but it might be worth looking at.

[jackfirth]

I see a ++convert flag, but not a --convert one. The ++convert one already accepts gifs I think. From what I can decipher it's only the prop:convertible mechanism that doesn't accept gifs, images added with @image{} can be png, svg, or gif.

[jackfirth]

Changed render-convertible-as? to allow gifs. Skipping tests since manual testing seems to work and I have no idea how to set up html rendering tests.

[mflatt]

Ok by me. Is it worth extracting the GIF width and height to include as attributes in the img?

[soegaard]

Den tor. 21. maj 2020 kl. 05.07 skrev Sam Tobin-Hochstadt < notifications@github.com>:

There's also the --convert flag, which should maybe also accept gif, and the render-convertible-as property. I don't know if it makes sense to change all these, but it might be worth looking at.

As far as I know, there is only one reason to use gifs namely to display animations. For all other purposes the existing image formats are better. Therefore a general convert-to-gif option isn't worth it. /Jens Axel

[jackfirth]

@mflatt Yes, that's a good idea. Will update the PR.

[jackfirth]

@mflatt Done!