Rewrite of the abbreviation feature.

* Fixes some bugs in multi-cursor scenarios. * Gets rid of several hacks by introducing a more general system. * Removes now obsolete command "lean.input.convertWithNewline". * Abbreviations are now replaced as soon as possible if the abbreviation is unique. * Adds mobx dependency and makes the abbreviation config observable.
leanprover · Jan 7, 2021 · 67e5d37 · 67e5d37
1 parent cafc38f
commit 67e5d37
Show file tree

Hide file tree

Showing 19 changed files with 8,848 additions and 371 deletions.
diff --git a/.eslintrc.js b/.eslintrc.js
@@ -116,7 +116,7 @@ module.exports = {
         "no-throw-literal": "error",
         "no-trailing-spaces": "error",
         "no-undef-init": "error",
-        "no-underscore-dangle": "error",
+        "no-underscore-dangle": "off",
         "no-unsafe-finally": "error",
         "no-unused-expressions": "error",
         "no-unused-labels": "error",