Upgrade to CodeMirror 6 release#1016

Merged

microbit-matt-hillsdon merged 8 commits intomainfrom

upgrade-codemirror

Oct 18, 2022

Commits on Oct 18, 2022

Upgrade to CodeMirror 6 release - first pass

microbit-robert
authored and
microbit-matt-hillsdon
committed
Tweaks

microbit-robert
authored and
microbit-matt-hillsdon
committed
Prevent autocomplete from closing on blur

microbit-robert
authored and
microbit-matt-hillsdon
committed
Use history API to navigate from autocomplete

microbit-robert
authored and
microbit-matt-hillsdon
committed
Revert "Use history API to navigate from autocomplete"

microbit-robert
authored and
microbit-matt-hillsdon
committed
Tidy

microbit-robert
authored and
microbit-matt-hillsdon
committed
No hover delay for gutter tooltips

microbit-robert
authored and
microbit-matt-hillsdon
committed
May we well have the very latest.
microbit-matt-hillsdon
committed