feat: customizable occurrence highlighting #371
Conversation
Makes it possible to disable substring-based occurrence highlighting and use only Lean's compiler responses.
david-christiansen
force-pushed
the
toggleable-text-highlight
branch
from
f171094 to
f2b7e77
Compare
| @@ -64,6 +64,21 @@ | |||
| "default": true, | |||
| "markdownDescription": "Enable eager replacement of abbreviations that uniquely identify a symbol." | |||
| }, | |||
| "lean4.editor.occurrenceHighlightingMode": { | |||
| "type": "string", | |||
| "description": "Highlight occurrences using Lean's semantic information, by string matching, or both", | |||
There was a problem hiding this comment.
| "description": "Highlight occurrences using Lean's semantic information, by string matching, or both", | |
| "description": "Highlight occurrences of a symbol using Lean's semantic information, by string matching, or both", |
Maybe slightly clearer as to what it is that's occurring?
There was a problem hiding this comment.
I intentionally avoided this phrasing because the string-based highlighting doesn't match symbols (which is why I want to turn it off - I find it undermines the usefulness of the highlights if I can't trust them). But perhaps I'm being too pedantic here.
How do you feel about the phrasing in #377?
There was a problem hiding this comment.
Gotcha! The other PR is worded well.
There was a problem hiding this comment.
Thanks! I tried hard to thread that needle, glad it succeeded
|
I think #377 is strictly better than this, but I'll leave it up to a maintainer to decide what to merge and what to close. |
|
Subsumed by the now merged #377. |
Makes it possible to disable substring-based occurrence highlighting and use only Lean's compiler responses.
I personally found the string-based highlighting to be distracting and confusing. This change defaults to semantic-only highlighting at @mhuisi 's request, so it will be user-visible.