Skip to content

Commit

Permalink
[doc] Document workspace folders PR (#374)
Browse files Browse the repository at this point in the history
  • Loading branch information
@ejgallego
ejgallego committed Feb 18, 2023
1 parent 174317f commit 3f69469
Show file tree
Hide file tree
Showing 2 changed files with 40 additions and 32 deletions.
7 changes: 7 additions & 0 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ interactive use, and provides extra features from vanilla Coq.
- [🗒️ Markdown Support](#️-markdown-support)
- [👥 Document Outline](#-document-outline)
- [🔎 Document Hover](#-document-hover)
- [📁️ Multiple Workspaces](#-multiple-workspaces)
- [⏱️ Detailed Timing and Memory Statistics](#️-detailed-timing-and-memory-statistics)
- [🔧 Client-Side Configuration Options](#-client-side-configuration-options)
- [♻️ Reusability, Standards, Modularity](#️-reusability-standards-modularity)
Expand Down Expand Up @@ -116,6 +117,12 @@ Hovering over a Coq identifier will show its type.

<img alt="Types on Hover" height="286px" src="etc/img/lsp-hover-2.gif"/>

### 📁 Multiple Workspaces

`coq-lsp` supports projects with multiple `_CoqProject` files, use the "Add
folder to Workspace" feature of Visual Studio code or the LSP Workspace Folders
extension to use this in your project.

### ⏱️ Detailed Timing and Memory Statistics

Hover over any Coq sentence, `coq-lsp` will display detailed memory and timing
Expand Down
65 changes: 33 additions & 32 deletions etc/doc/PROTOCOL.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,38 +16,39 @@ https://github.com/microsoft/language-server-protocol/issues/1414

If a feature doesn't appear here it usually means it is not planned in the short term:

| Method | Support | Notes |
|-----------------------------------|---------|------------------------------------------------------------|
| `initialize` | Partial | We don't obey the advertised client capabilities |
| `client/registerCapability` | No | Not planned ATM |
| `$/setTrace` | Yes | |
| `$/logTrace` | Yes | |
| `window/logMessage` | Yes | |
|-----------------------------------|---------|------------------------------------------------------------|
| `textDocument/didOpen` | Yes | We can't reuse Memo tables yet |
| `textDocument/didChange` | Yes | We only support `TextDocumentSyncKind.Full` for now |
| `textDocument/didClose` | Partial | We'd likely want to save a `.vo` file on close if possible |
| `textDocument/didSave` | No | |
|-----------------------------------|---------|------------------------------------------------------------|
| `notebookDocument/didOpen` | No | Planned |
|-----------------------------------|---------|------------------------------------------------------------|
| `textDocument/declaration` | No | Planned, blocked on upstream issues |
| `textDocument/definition` | Partial | Working only locally on files for now |
| `textDocument/references` | No | Planned, blocked on upstream issues |
| `textDocument/hover` | Yes | Shows stats and type info of identifiers at point |
| `textDocument/codeLens` | No | |
| `textDocument/foldingRange` | No | |
| `textDocument/documentSymbol` | Yes | Sections and modules missing (#322) |
| `textDocument/semanticTokens` | No | Planned |
| `textDocument/inlineValue` | No | Planned |
| `textDocument/inlayHint` | No | Planned |
| `textDocument/completion` | Partial | Needs more work locally and upstream (#50) |
| `textDocument/publishDiagnostics` | Yes | |
| `textDocument/diagnostic` | No | Planned, issue #49 |
| `textDocument/codeAction` | No | Planned |
|-----------------------------------|---------|------------------------------------------------------------|
| `workspace/workspaceFolders` | No | |
|-----------------------------------|---------|------------------------------------------------------------|
| Method | Support | Notes |
|---------------------------------------|---------|------------------------------------------------------------|
| `initialize` | Partial | We don't obey the advertised client capabilities |
| `client/registerCapability` | No | Not planned ATM |
| `$/setTrace` | Yes | |
| `$/logTrace` | Yes | |
| `window/logMessage` | Yes | |
|---------------------------------------|---------|------------------------------------------------------------|
| `textDocument/didOpen` | Yes | We can't reuse Memo tables yet |
| `textDocument/didChange` | Yes | We only support `TextDocumentSyncKind.Full` for now |
| `textDocument/didClose` | Partial | We'd likely want to save a `.vo` file on close if possible |
| `textDocument/didSave` | No | Not clear what to do here yet |
|---------------------------------------|---------|------------------------------------------------------------|
| `notebookDocument/didOpen` | No | Planned |
|---------------------------------------|---------|------------------------------------------------------------|
| `textDocument/declaration` | No | Planned, blocked on upstream issues |
| `textDocument/definition` | Partial | Working only locally on files for now |
| `textDocument/references` | No | Planned, blocked on upstream issues |
| `textDocument/hover` | Yes | Shows stats and type info of identifiers at point |
| `textDocument/codeLens` | No | |
| `textDocument/foldingRange` | No | |
| `textDocument/documentSymbol` | Yes | Sections and modules missing (#322) |
| `textDocument/semanticTokens` | No | Planned |
| `textDocument/inlineValue` | No | Planned |
| `textDocument/inlayHint` | No | Planned |
| `textDocument/completion` | Partial | Needs more work locally and upstream (#50) |
| `textDocument/publishDiagnostics` | Yes | |
| `textDocument/diagnostic` | No | Planned, issue #49 |
| `textDocument/codeAction` | No | Planned |
|---------------------------------------|---------|------------------------------------------------------------|
| `workspace/workspaceFolders` | Yes | Each folder should have a `_CoqProject` file at the root. |
| `workspace/didChangeWorkspaceFolders` | Yes | |
|---------------------------------------|---------|------------------------------------------------------------|

### URIs accepted by coq-lsp

Expand Down

0 comments on commit 3f69469

Please sign in to comment.