feat: manual (#453)

This PR adds an extensive manual for the Lean 4 VS Code extension and central parts of the Lean 4 language server. It also covers general VS Code features that Lean users who have not used VS Code before may find to be helpful when working with Lean. There are still some obvious improvements to the manual view that would be nice to have, but I hope that this is at least a good start. ![ToC](https://github.com/leanprover/vscode-lean4/assets/10852073/de2cca46-dc6f-4217-b610-4a85fec0bced)
leanprover · May 23, 2024 · 451c7d4 · 451c7d4
1 parent 7211eca
commit 451c7d4
Show file tree

Hide file tree

Showing 54 changed files with 838 additions and 51 deletions.
diff --git a/package-lock.json b/package-lock.json
diff --git a/vscode-lean4/media/abbreviation.png b/vscode-lean4/media/abbreviation.png
diff --git a/vscode-lean4/media/breadcrumbs.png b/vscode-lean4/media/breadcrumbs.png
diff --git a/vscode-lean4/media/call-hierarchy-outgoing.png b/vscode-lean4/media/call-hierarchy-outgoing.png
diff --git a/vscode-lean4/media/call-hierarchy.png b/vscode-lean4/media/call-hierarchy.png
diff --git a/vscode-lean4/media/code-action.png b/vscode-lean4/media/code-action.png
diff --git a/vscode-lean4/media/code-folding.png b/vscode-lean4/media/code-folding.png
diff --git a/vscode-lean4/media/command-menu.png b/vscode-lean4/media/command-menu.png
diff --git a/vscode-lean4/media/command-palette.png b/vscode-lean4/media/command-palette.png
diff --git a/vscode-lean4/media/completion.png b/vscode-lean4/media/completion.png
diff --git a/vscode-lean4/media/diagnostics.png b/vscode-lean4/media/diagnostics.png
diff --git a/vscode-lean4/media/document-outline.png b/vscode-lean4/media/document-outline.png
diff --git a/vscode-lean4/media/file-explorer.png b/vscode-lean4/media/file-explorer.png
diff --git a/vscode-lean4/media/file-progress.png b/vscode-lean4/media/file-progress.png
diff --git a/vscode-lean4/media/find-references.png b/vscode-lean4/media/find-references.png
diff --git a/vscode-lean4/media/go-to-file.png b/vscode-lean4/media/go-to-file.png
diff --git a/vscode-lean4/media/go-to-symbol.png b/vscode-lean4/media/go-to-symbol.png
diff --git a/vscode-lean4/media/guide-vscode.md b/vscode-lean4/media/guide-vscode.md
@@ -1,30 +1,3 @@
 ## Using Lean 4 in VS Code
 
-**Working with multiple files**  
-When working on a Lean 4 file `A.lean` that imports another Lean 4 file `B.lean`, you will notice that changes to `B.lean` do not automatically appear in `A.lean`.
-To make them appear, select the tab for `A.lean`, click on the ∀-symbol in the top right and select 'Server: Restart File' (Ctrl+Shift+X).
-This manual interaction helps to prevent accidental and potentially expensive rebuilds of the project.
-
-  ![Restart File](restart-file.png)
-
-**Inputting Unicode Symbols**  
-You can input Unicode symbols in Lean 4 files by typing a backslash (`\`) character followed by the name of the Unicode symbol.
-For example, `\all` becomes `∀` and `\Nat` becomes `ℕ`.
-
-If you encounter a Unicode symbol in Lean 4 code and want to learn how to type it, you can hover over the symbol with your mouse and it will display the name of the Unicode symbol.
-
-  ![Unicode Hover](unicode-hover.png)
-
-A full list of all Unicode symbol names can be found by clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Docview: Show All Abbreviations'.
-
-**Navigating Lean 4 Code**  
-Right-clicking on any identifer will bring up the following context menu:
-
-  ![Context Menu](context-menu.png)
-
-The two most important entries in this list are 'Go to Definition' and 'Find All References'.  
-'Go to Definition' will take you to the file that defines the identifier, whereas 'Find All References' will display all locations where the identifier is used.
-
-If you know the name of an identifier but are not sure where to find it, you can open the symbol search by hitting 'Ctrl+P' and typing in `#` followed by the name of the identifier. The search will bring up all identifiers containing the given name and clicking on any of the results will take you to the file where it is defined.
-
-  ![Symbol Search](symbol-search.png)
+The [Lean 4 VS Code extension manual](command:lean4.setup.showExtensionManual) covers all kinds of essential tools when working with Lean 4 in VS Code. Even if you are already familiar with other programming languages and VS Code in general, you may find the first five subsections of the 'Interacting with Lean files' section in the manual to be very helpful. 
diff --git a/vscode-lean4/media/hover.png b/vscode-lean4/media/hover.png
diff --git a/vscode-lean4/media/identifier-context-menu.png b/vscode-lean4/media/identifier-context-menu.png
diff --git a/vscode-lean4/media/infoview-go-to-definition.png b/vscode-lean4/media/infoview-go-to-definition.png
diff --git a/vscode-lean4/media/infoview-hover.png b/vscode-lean4/media/infoview-hover.png
diff --git a/vscode-lean4/media/infoview.png b/vscode-lean4/media/infoview.png