See src/Code.html for details.