From 44b7def9bf8d5b85cb969e10c5f68b45d502d974 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 21 Oct 2024 13:19:21 +0200 Subject: [PATCH] doc: list default settings and how to override them in the manual (#540) Closes #539. --- vscode-lean4/manual/manual.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md index 9f1f5837b..347e826bb 100644 --- a/vscode-lean4/manual/manual.md +++ b/vscode-lean4/manual/manual.md @@ -62,6 +62,17 @@ Settings of the Lean 4 VS Code extension and VS Code itself can be configured in The specific settings of the Lean 4 VS Code extension are described in detail in later sections. +The Lean 4 VS Code extensions sets a number of default settings for Lean 4 documents: +- **'Editor: Insert Spaces': true**. Pressing `Tab` will insert spaces. +- **'Editor: Tab Size': 2**. Pressing `Tab` will insert two spaces. +- **'Files: Encoding': UTF-8**. Files use the [UTF-8 encoding](https://en.wikipedia.org/wiki/UTF-8). +- **'Files: Eol': \n**. All lines use `\n` as the line break symbol for consistency between Windows and Unix based operating systems. +- **'Files: Insert Final Newline': true**. All files are terminated by an empty line. +- **'Files: Trim Final Newlines': true**. There is only a single empty line at the end of each file. +- **'Files: Trim Trailing Whitespace': true**. There is no redundant whitespace at the end of a line. + +It is recommended to leave these settings at their default. Nonetheless, these default settings can be overriden in the ['Settings' page of VS Code](command:workbench.action.openSettings2) by first entering `@lang:lean4` into the settings search bar and then changing the respective setting. +
| ![](images/settings_page.png) |