Closes #3791

Issue #3423

... and export (via defineExtension) a method to explicitly trigger
linting from user code.

- Link to external jsonlint.js (don't want dependencies in repo if
  I can help it)

- Use a single demo file (prevent demo/ from becoming a huge mess)

- Make whitespace and newlines conform to other files, fix linter errors

Since these no longer follow directly from scroller.clientHeight/Width.

Use these to ensure messages for current line are scrolled into view
in demo/widget.html.

Closes #802

Instead of a single 'inline' option, add noHScroll and coverGutter options.

This seems to be a better fix for the scroll artifacts.

Closes #795

There's apparently a timing issue with adding widgets to
a just-initialized editor.

The off pun is rather awful, but it does have precedent, and is
more succinct.