Mostly done, apart from some polishing, as of 5f5c545.
5f5c545
Superseded by #456. This comment was generated automatically.