From 61cadad140b63b79796fc98038f639e5610adbda Mon Sep 17 00:00:00 2001 From: Jaehwang Jung Date: Mon, 27 Nov 2023 00:28:06 +0900 Subject: [PATCH] Update docs --- docs/protocol.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/protocol.md b/docs/protocol.md index ddcf8929e..7384a4e3f 100644 --- a/docs/protocol.md +++ b/docs/protocol.md @@ -104,14 +104,14 @@ For providing highlights which reflect the current internal state of coq, we pro interface UpdateHighlightsNotification { //Document idefinfier 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 and processed range correspond to the ranges of lines in the document that have the coresponding type. +The processing 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