Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

update docs and fix typo #690

Merged
merged 2 commits into from
Nov 22, 2023
Merged

update docs and fix typo #690

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
af10e22
update docs and fix typo
tomtomjhj Nov 20, 2023
74f2c25
Update client/src/protocol/types.ts
rtetley Nov 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions client/src/protocol/types.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,9 +51,9 @@ export interface ProofViewNotification {
messages: CoqMessage[];
}

export interface UpdateHightlightsNotification {
export interface UpdateHighlightsNotification {
uri: Uri;
parsedRange: Range[];
processingRange: Range[];
processedRange: Range[];
}

Expand Down
22 changes: 6 additions & 16 deletions docs/protocol.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,19 +101,17 @@ interface Configuration {
For providing highlights which reflect the current internal state of coq, we provide "vscoq/updateHighlights" which returns an object containing

``` typescript
interface Highlights {
interface UpdateHighlightsNotification {
//Document idefinfier
uri: TextDocumentIdentifier;
uri: Uri;
// The ranges of lines of code that were parsed by the server
parsedRange: vscode.Range[];
// The ranges of lines of code currently being processed by the server
processingRange: vscode.Range[];
// The ranges of lines of code that have been processed by the server
processedRange: vscode.Range[];
}
```

The parsed, processing and processed range correspond to the ranges of lines in the document that have the coresponding type.
The parsed and processed range correspond to the ranges of lines in the document that have the coresponding type.
By default, we display the processed lines in the VSCode gutter.

## Goal view
Expand Down Expand Up @@ -201,11 +199,6 @@ interface SearchCoqRequest {
interface SearchCoqHandshake {
//Returns the provided uuid
id: string;
//If the search was succesful just returns ok
result?: boolean;
//Returns any relevant error message
error?: any;

}

interface SearchCoqResult {
Expand All @@ -218,19 +211,17 @@ interface SearchCoqResult {
}
```

By default the coq Search command as asynchronous. Therefore, the language server first sends a handshake either with an OK code, or with an error. It then sends each result one by one through the SearchCoqResult interface. The id corresponds to a uuid given to each search request.
By default the coq Search command as asynchronous. Therefore, the language server first sends a handshake either with an OK code, or with an error. It then sends each result one by one through the SearchCoqResult notification. The id corresponds to a uuid given to each search request.

We also provide the requests for the "check", "about", "locate" and "print" queries, with plans to support more in the future.
Note that the "check" and about "about" queries are synchronous and do not require a seperate verb for their responses.
Verbs: `vscoq/check`, `vscoq/about`.
We also provide the requests for the `vscoq/check`, `vscoq/about`, `vscoq/locate` and `vscoq/print` queries, with plans to support more in the future.
These queries are synchronous and do not require a seperate verb for their responses.

```typescript

interface AboutCoqRequest {
textDocument: VersionedTextDocumentIdentifier;
pattern: string;
position: Position;
goalIndex?: number;
}

type AboutCoqResponse = PpString;
Expand All @@ -239,7 +230,6 @@ interface CheckCoqRequest {
textDocument: VersionedTextDocumentIdentifier;
pattern: string;
position: Position;
goalIndex?: number;
};

type CheckCoqResponse = PpString;
Expand Down
Loading