Wolfgang Jeltsch (Aug 07 2023 at 12:59): Wolfgang Jeltsch (Aug 07 2023 at 12:59):By default, Isabelle/VSCode (from Isabelle2022) will flood you with suggestion popups regarding possible completions of English words, at least when writing some documentation text. I tried to disable that and already found the “Suggest: Show Words” option. However, deactivating this only got me rid of the suggestions of words I have typed myself elsewhere. I still get the popups that tell me that instead of “what” I could write “who” and that ask me whether I want to exclude the word I’m typing, perhaps permanently. It seems these suggestions are linked to some (English) dictionary. I’ve already searched the web back and forth regarding how to disable these but to no avail. Any help would be greatly appreciated.
Last updated: May 02 2024 at 04:18 UTC