DEFAULT_HOVER_TIME

Default hover delay, in milliseconds, used by the async hoverTooltip overload. Mirrors upstream CodeMirror's hoverTime default.