warning upon detection of tab characters

[johnyf]

Space characters are used in TLA+, and tabs avoided. tlapm does not parse tabs (https://github.com/tlaplus/tlapm/issues/28). The TLA+ VSCode extension converts input from the tab key to 4 space characters. Changing the editor settings "Detect Indentation" and "Insert Spaces" of VSCode, I observe that the TLA+ VSCode extension continues to insert spaces (as intended). I would like to ask whether there is any way to insert tab characters, other than pasting the tab characters.

It might also be useful to warn in case tab characters are detected in the current file, upon opening the file, or as new tab characters during editing (e.g., due to copy/pasting lines from elsewhere). I do not know how extensive a change it would be to implement such a warning mechanism.

This issue is relevant to https://github.com/tlaplus/tlaplus/issues/655.

The VSCode editor options mentioned above are described in VSCode as follows:

• Editor: Detect Indentation

  Controls whether Editor: Tab size and Editor: Insert Spaces will be automatically detected when a file is opened based on the file contents.

• Editor: Insert Spaces

  Insert spaces when pressing Tab. This setting is overridden based on the file contents when Editor: Detection Indentation is on.

Areas of code that seem relevant to this issue:

https://github.com/alygin/vscode-tlaplus/blob/8b31c784fd10faecd3791c7a7181e3007fdcf568/package.json#L362-L373

https://github.com/alygin/vscode-tlaplus/blob/8b31c784fd10faecd3791c7a7181e3007fdcf568/src/formatters/formatting.ts#L81-L82

https://github.com/alygin/vscode-tlaplus/blob/8b31c784fd10faecd3791c7a7181e3007fdcf568/tests/suite/formatters/formatting.ts#L6-L9

https://github.com/alygin/vscode-tlaplus/blob/8b31c784fd10faecd3791c7a7181e3007fdcf568/tests/suite/formatters/tla.test.ts#L604-L635