Formalize patching of `book.js`

Inspired by #2571 and other similar changes I made myself, we need to come up with a proper system for maintaining our customizations to `theme/book.js`. That is, we need to store our modifications as patches or something very similar. Right now, our customizations are direct edits to the file.

The problem is that `mdbook` is somewhat coupled to it's theme: when we update `mdbook` to a new version, we run the risk of messing up the rendering if we don't update our (partial!) copy of the default theme.

I'm imagining a system where we:

1. Store the modifications as a set of patches.
2. Check that `theme/book.js` is truly equal to the original `book.js` file plus the applied patches in a GitHub action.
3. Some script which can update our `mdbook` version by updating the `book.js` file.

I'm probably missing some steps here! 😄

Cc @djmitche, @gribozavr.