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 · Dec 30, 2020 · c564341 · c564341
1 parent 7e99440
commit c564341
Show file tree

Hide file tree

Showing 20 changed files with 4,132 additions and 2,239 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",