clarified abbreviation;

tuned whitespace;

tuned;

more NEWS;

more inner syntax markup: HOL-Analysis;

tuned markup;

more inner syntax markup: HOLCF;

more 'no_syntax' bundles;

more robust 'no_syntax' via bundles;

tuned markup;

drop somewhat pointless 'syntax_consts' declarations;

clarified syntax: use outer block (with indent);

clarified syntax: prefer nonterminal "args", use outer block (with indent);

proper command kinds;

updated vscode_extension;

NEWS and CONTRIBUTORS;

clarified: add operation;

minor tuning;

lsp: added additional commit characters to immediate completions;

vscode: further adjusted default settings and wordPattern for consistent completion popups; for some reason wordPattern must be set to match (almost) everything, otherwise completions only pop up every other character, and then we must disable wordBasedSuggestions or it will suggest whole lines out of the document;

lsp: added more triggerCharacters to make completion popups more consistent;

vscode: added default setting to make completions pop up by themselves;

lsp: improved completions;

vscode: removed unused code;

vscode: removed README because its content is outdated;

vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;

lsp: added symbol conversion request;

vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;