This change updates our docs builder to prefer documentation included by

the new @webapi_docs decorator instead of relying purely on docstrings.

Migrated some API documentation out of docstrings into @webapi_docs and

built the user manual. Checked that the API documentation was correct.