Add codemirror keybindings and addons (#311)

* added codemirror addons
- fullScreen
- autorefresh
added a default:
- extraKeys

Co-authored-by: Tilman Vatteroth <tilman.vatteroth@tu-dortmund.de>
Co-authored-by: mrdrogdrog <mr.drogdrog@gmail.com>
Co-authored-by: Erik Michelson <github@erik.michelson.eu>
This commit is contained in:
Philip Molares 2020-08-06 13:43:48 +02:00 committed by GitHub
parent dbce0181a4
commit fc2e2bd592
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
12 changed files with 1758 additions and 382 deletions

View file

@ -0,0 +1,8 @@
import 'codemirror'
declare module 'codemirror' {
// noinspection JSUnusedGlobalSymbols
interface EditorConfiguration {
fullScreen?: boolean;
}
}