From d3e5dee1d69da47ca04263b364a175b0aa28b53b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 26 Dec 2022 02:13:25 +0100
Subject: [PATCH 1/2] [fleche] `_end` -> `end_` in Types.Range.t

This was a silly mistake, `_end` is convention for unused.

(I'm a bit "dislexic" with this stuff)
---
 fleche/info.ml   | 8 ++++----
 fleche/types.ml  | 4 ++--
 fleche/types.mli | 2 +-
 lsp/base.ml      | 4 ++--
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/fleche/info.ml b/fleche/info.ml
index 55849344..02e17419 100644
--- a/fleche/info.ml
+++ b/fleche/info.ml
@@ -56,8 +56,8 @@ module LineCol : Point with type t = int * int = struct
       let r = Types.to_range loc in
       let line1 = r.start.line in
       let col1 = r.start.character in
-      let line2 = r._end.line in
-      let col2 = r._end.character in
+      let line2 = r.end_.line in
+      let col2 = r.end_.character in
       if debug_in_range then
         Io.Log.error "in_range"
           (Format.asprintf "(%d, %d) in (%d,%d)-(%d,%d)" line col line1 col1
@@ -74,8 +74,8 @@ module LineCol : Point with type t = int * int = struct
       let r = Types.to_range loc in
       let line1 = r.start.line in
       let col1 = r.start.character in
-      let line2 = r._end.line in
-      let col2 = r._end.character in
+      let line2 = r.end_.line in
+      let col2 = r.end_.character in
       if debug_in_range then
         Io.Log.error "gt_range"
           (Format.asprintf "(%d, %d) in (%d,%d)-(%d,%d)" line col line1 col1
diff --git a/fleche/types.ml b/fleche/types.ml
index b60b6e1f..2d4bbed5 100644
--- a/fleche/types.ml
+++ b/fleche/types.ml
@@ -27,7 +27,7 @@ end
 module Range = struct
   type t =
     { start : Point.t
-    ; _end : Point.t
+    ; end_ : Point.t
     }
 end
 
@@ -56,7 +56,7 @@ let to_range (p : Loc.t) : Range.t =
   let end_col = ep - bol_pos_last in
   Range.
     { start = { line = start_line; character = start_col; offset = bp }
-    ; _end = { line = end_line; character = end_col; offset = ep }
+    ; end_ = { line = end_line; character = end_col; offset = ep }
     }
 
 let to_orange = Option.map to_range
diff --git a/fleche/types.mli b/fleche/types.mli
index 756e6cb5..652120b0 100644
--- a/fleche/types.mli
+++ b/fleche/types.mli
@@ -26,7 +26,7 @@ end
 module Range : sig
   type t =
     { start : Point.t
-    ; _end : Point.t
+    ; end_ : Point.t
     }
 end
 
diff --git a/lsp/base.ml b/lsp/base.ml
index 5d640b58..7dbab7a2 100644
--- a/lsp/base.ml
+++ b/lsp/base.ml
@@ -50,13 +50,13 @@ let mk_notification ~method_ ~params =
    let json_of_thm thm = let open Proofs in match thm with | None -> `Null |
    Some thm -> `Assoc [ "goals", `List List.(map json_of_goal thm.t_goals) ] *)
 
-let mk_range { Fleche.Types.Range.start; _end } : J.t =
+let mk_range { Fleche.Types.Range.start; end_ } : J.t =
   `Assoc
     [ ( "start"
       , `Assoc
           [ ("line", `Int start.line); ("character", `Int start.character) ] )
     ; ( "end"
-      , `Assoc [ ("line", `Int _end.line); ("character", `Int _end.character) ]
+      , `Assoc [ ("line", `Int end_.line); ("character", `Int end_.character) ]
       )
     ]
 

From 8ebe84be963a87fe26023907ccbf38b7f3f0fb36 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 26 Dec 2022 02:11:36 +0100
Subject: [PATCH 2/2] [fleche] Implement fileProgress notification for document
 progress

This is modelled after Lean's `$/lean/fileProgress` notification: a
yellow bar in the right side panel indicates what parts of the
document are still not checked.

Fixes #54

Note that we send on fileProgress per sentence, that's likely too
much; for now, we throttle the decoration update. Could be made into a
user-config.
---
 CHANGES.md                    |   3 +
 README.md                     |   6 ++
 controller/coq_lsp.ml         |  37 ++++++++--
 editor/code/package-lock.json |  27 ++++++++
 editor/code/package.json      |   3 +-
 editor/code/src/client.ts     |  32 ++++++++-
 editor/code/src/goals.ts      |   1 +
 editor/code/src/progress.ts   |  26 +++++++
 etc/doc/PROTOCOL.md           | 125 ++++++++++++++++++++++++++++++++++
 fleche/debug.ml               |   3 +
 fleche/doc.ml                 |  73 ++++++++++++++++----
 fleche/doc.mli                |   7 +-
 fleche/io.ml                  |   6 ++
 fleche/io.mli                 |   5 ++
 14 files changed, 328 insertions(+), 26 deletions(-)
 create mode 100644 editor/code/src/progress.ts
 create mode 100644 etc/doc/PROTOCOL.md

diff --git a/CHANGES.md b/CHANGES.md
index 266e618d..389d5fa0 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -13,6 +13,9 @@
  - Don't convert Coq "Info" messages such as "Foo is defined" to
    feedback by default; users willing to see them can set the
    corresponding option (@ejgallego, #113)
+ - Send `$/coq/fileProgress` progress notifications from server,
+   similarly to what Lean does; display them in Code's right gutter
+   (@ejgallego, #106, fixes #54)
 
 # coq-lsp 0.1.0: Memory
 -----------------------
diff --git a/README.md b/README.md
index acbf95c6..3556d0ff 100644
--- a/README.md
+++ b/README.md
@@ -150,6 +150,12 @@ Supporting inlays and Lean-style info view.
 
 ### Suggestions / Search panel
 
+## Protocol Notes
+
+`coq-lsp` mostly implements the [LSP Standard](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/), plus some extensions specific to Coq.
+
+Check [the `coq-lsp` protocol documentation](etc/doc/PROTOCOL.md) for more details.
+
 ## Development / Building from sources
 
 ### Server:
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 06d2ceb0..0fa9c222 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -138,6 +138,21 @@ let lsp_of_diags ~uri ~version diags =
     diags
   |> LSP.mk_diagnostics ~uri ~version
 
+let lsp_of_progress ~uri ~version progress =
+  let progress =
+    List.map
+      (fun (range, kind) ->
+        `Assoc [ ("range", LSP.mk_range range); ("kind", `Int kind) ])
+      progress
+  in
+  let params =
+    [ ( "textDocument"
+      , `Assoc [ ("uri", `String uri); ("version", `Int version) ] )
+    ; ("processing", `List progress)
+    ]
+  in
+  LSP.mk_notification ~method_:"$/coq/fileProgress" ~params
+
 let asts_of_doc doc =
   List.filter_map (fun v -> v.Fleche.Doc.ast) doc.Fleche.Doc.nodes
 
@@ -158,7 +173,9 @@ module Check = struct
 
   let completed uri =
     let doc = Hashtbl.find doc_table uri in
-    doc.completed = Yes
+    match doc.completed with
+    | Yes _ -> true
+    | _ -> false
 
   let schedule ~uri = pending := Some uri
 end
@@ -186,7 +203,6 @@ let do_change params =
   let uri, version =
     (string_field "uri" document, int_field "version" document)
   in
-  Log.log_error "checking file" (uri ^ " / version: " ^ string_of_int version);
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
   | [] -> ()
@@ -195,12 +211,18 @@ let do_change params =
       "more than one change unsupported due to sync method";
     assert false
   | change :: _ ->
-    let text = string_field "text" change in
+    let contents = string_field "text" change in
     let doc = Hashtbl.find doc_table uri in
     let doc =
       (* [bump_version] will clean stale info about the document, in particular
          partial results of a previous checking *)
-      if version > doc.version then Fleche.Doc.bump_version ~version ~text doc
+      if version > doc.version then (
+        Log.log_error "bump file" (uri ^ " / version: " ^ string_of_int version);
+        let tb = Unix.gettimeofday () in
+        let doc = Fleche.Doc.bump_version ~version ~contents doc in
+        let diff = Unix.gettimeofday () -. tb in
+        Log.log_error "bump file took" (Format.asprintf "%f" diff);
+        doc)
       else doc
     in
     let () = Hashtbl.replace doc_table uri doc in
@@ -352,6 +374,8 @@ let memo_read_from_disk () = if false then memo_read_from_disk ()
 let request_queue = Queue.create ()
 
 let process_input (com : J.t) =
+  if Fleche.Debug.sched_wakeup then
+    Log.log_error "-> enqueue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
   (* TODO: this is the place to cancel pending requests that are invalid, and in
      general, to perform queue optimizations *)
   Queue.push com request_queue;
@@ -402,6 +426,8 @@ let dispatch_message ofmt ~state dict =
     Log.log_error "BT" bt
 
 let rec process_queue ofmt ~state =
+  if Fleche.Debug.sched_wakeup then
+    Log.log_error "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
   (match Queue.peek_opt request_queue with
   | None -> (
     match !Check.pending with
@@ -429,6 +455,9 @@ let lsp_cb oc =
     ; send_diagnostics =
         (fun ~uri ~version diags ->
           lsp_of_diags ~uri ~version diags |> Lsp.Io.send_json oc)
+    ; send_fileProgress =
+        (fun ~uri ~version progress ->
+          lsp_of_progress ~uri ~version progress |> Lsp.Io.send_json oc)
     }
 
 let lvl_to_severity (lvl : Feedback.level) =
diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json
index e2e8333e..5b80db2c 100644
--- a/editor/code/package-lock.json
+++ b/editor/code/package-lock.json
@@ -8,10 +8,12 @@
       "name": "coq-lsp",
       "version": "0.1.0",
       "dependencies": {
+        "throttle-debounce": "^5.0.0",
         "vscode-languageclient": "^8.0.2"
       },
       "devDependencies": {
         "@types/node": "^10.14.15",
+        "@types/throttle-debounce": "^5.0.0",
         "@types/vscode": "^1.73.0",
         "esbuild": "^0.15.14",
         "typescript": "^4.8.4"
@@ -58,6 +60,12 @@
       "integrity": "sha512-F0KIgDJfy2nA3zMLmWGKxcH2ZVEtCZXHHdOQs2gSaQ27+lNeEfGxzkIw90aXswATX7AZ33tahPbzy6KAfUreVw==",
       "dev": true
     },
+    "node_modules/@types/throttle-debounce": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/@types/throttle-debounce/-/throttle-debounce-5.0.0.tgz",
+      "integrity": "sha512-Pb7k35iCGFcGPECoNE4DYp3Oyf2xcTd3FbFQxXUI9hEYKUl6YX+KLf7HrBmgVcD05nl50LIH6i+80js4iYmWbw==",
+      "dev": true
+    },
     "node_modules/@types/vscode": {
       "version": "1.73.0",
       "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.73.0.tgz",
@@ -476,6 +484,14 @@
         "node": ">=10"
       }
     },
+    "node_modules/throttle-debounce": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/throttle-debounce/-/throttle-debounce-5.0.0.tgz",
+      "integrity": "sha512-2iQTSgkkc1Zyk0MeVrt/3BvuOXYPl/R8Z0U2xxo9rjwNciaHDG3R+Lm6dh4EeUci49DanvBnuqI6jshoQQRGEg==",
+      "engines": {
+        "node": ">=12.22"
+      }
+    },
     "node_modules/typescript": {
       "version": "4.8.4",
       "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.8.4.tgz",
@@ -551,6 +567,12 @@
       "integrity": "sha512-F0KIgDJfy2nA3zMLmWGKxcH2ZVEtCZXHHdOQs2gSaQ27+lNeEfGxzkIw90aXswATX7AZ33tahPbzy6KAfUreVw==",
       "dev": true
     },
+    "@types/throttle-debounce": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/@types/throttle-debounce/-/throttle-debounce-5.0.0.tgz",
+      "integrity": "sha512-Pb7k35iCGFcGPECoNE4DYp3Oyf2xcTd3FbFQxXUI9hEYKUl6YX+KLf7HrBmgVcD05nl50LIH6i+80js4iYmWbw==",
+      "dev": true
+    },
     "@types/vscode": {
       "version": "1.73.0",
       "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.73.0.tgz",
@@ -770,6 +792,11 @@
         "lru-cache": "^6.0.0"
       }
     },
+    "throttle-debounce": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/throttle-debounce/-/throttle-debounce-5.0.0.tgz",
+      "integrity": "sha512-2iQTSgkkc1Zyk0MeVrt/3BvuOXYPl/R8Z0U2xxo9rjwNciaHDG3R+Lm6dh4EeUci49DanvBnuqI6jshoQQRGEg=="
+    },
     "typescript": {
       "version": "4.8.4",
       "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.8.4.tgz",
diff --git a/editor/code/package.json b/editor/code/package.json
index 77080cc5..1d09e8f5 100644
--- a/editor/code/package.json
+++ b/editor/code/package.json
@@ -9,7 +9,6 @@
     "Shachar Itzhaky <shachari@cs.technion.ac.il>",
     "Ramkumar Ramachandra <r@artagnon.com>"
   ],
-
   "publisher": "ejgallego",
   "engines": {
     "vscode": "^1.73.0"
@@ -131,11 +130,13 @@
   },
   "devDependencies": {
     "@types/node": "^10.14.15",
+    "@types/throttle-debounce": "^5.0.0",
     "@types/vscode": "^1.73.0",
     "esbuild": "^0.15.14",
     "typescript": "^4.8.4"
   },
   "dependencies": {
+    "throttle-debounce": "^5.0.0",
     "vscode-languageclient": "^8.0.2"
   },
   "main": "./out/src/client.js",
diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
index 0a6c22c2..936e8531 100644
--- a/editor/code/src/client.ts
+++ b/editor/code/src/client.ts
@@ -1,3 +1,4 @@
+import { throttle } from "throttle-debounce";
 import {
     window,
     commands,
@@ -6,13 +7,17 @@ import {
     ViewColumn,
     Uri,
     TextEditor,
+    OverviewRulerLane
 } from "vscode";
-import {
+import * as vscode from "vscode";
+import { Range } from "vscode-languageclient";
+import { 
     LanguageClient,
     LanguageClientOptions,
     RevealOutputChannelOn,
 } from "vscode-languageclient/node";
 import { GoalPanel } from "./goals";
+import { coqFileProgress, CoqFileProgressParams } from "./progress";
 
 let client: LanguageClient;
 let goalPanel: GoalPanel | null;
@@ -45,7 +50,7 @@ export function activate(context: ExtensionContext): void {
             if (goalPanel) goalPanel.dispose();
         }
 
-        window.showInformationMessage("Going to start!");
+        window.showInformationMessage("Coq Language Server: starting");
 
         const config = workspace.getConfiguration("coq-lsp");
         const initializationOptions = {
@@ -69,16 +74,37 @@ export function activate(context: ExtensionContext): void {
         );
         client.start();
 
+        client.onNotification(coqFileProgress, (params) => {
+            let ranges = params.processing.map((fp) => rangeProto2Code(fp.range))
+                                          .filter((r) => ! r.isEmpty);
+            updateDecos(params.textDocument.uri, ranges);
+        });
+
         // XXX: Fix this mess with the lifetime of the panel
         goalPanel = panelFactory(context);
     };
+    const progressDecoration = window.createTextEditorDecorationType(
+        { overviewRulerColor: 'rgba(255,165,0,0.5)', overviewRulerLane: OverviewRulerLane.Left}
+    );
 
+    const updateDecos = throttle(200,
+        function(uri : string, ranges : vscode.Range[]) {
+            for (const editor of window.visibleTextEditors) {
+                if (editor.document.uri.toString() == uri) {
+                    editor.setDecorations(progressDecoration, ranges);
+                }
+            }
+        });
+
+    const rangeProto2Code = function(r : Range) {
+        return new vscode.Range(r.start.line, r.start.character, r.end.line, r.end.character);
+    };
     const checkPanelAlive = () => {
         if (!goalPanel) {
             goalPanel = panelFactory(context);
         }
     };
-    
+
     const goals = (editor : TextEditor) => {
         checkPanelAlive();
         let uri = editor.document.uri;
diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
index 935b77be..ae8c1125 100644
--- a/editor/code/src/goals.ts
+++ b/editor/code/src/goals.ts
@@ -10,6 +10,7 @@ interface Goal {
     ty: string;
     hyps: Hyp[];
 }
+
 interface GoalRequest {}
 
 // returns the HTML code of goals environment
diff --git a/editor/code/src/progress.ts b/editor/code/src/progress.ts
new file mode 100644
index 00000000..355cdce8
--- /dev/null
+++ b/editor/code/src/progress.ts
@@ -0,0 +1,26 @@
+import { NotificationType, NotificationType1, VersionedTextDocumentIdentifier, Range } from "vscode-languageclient";
+
+enum CoqFileProgressKind {
+    Processing = 1,
+    FatalError = 2
+}
+
+interface CoqFileProgressProcessingInfo {
+    /** Range for which the processing info was reported. */
+    range: Range;
+    /** Kind of progress that was reported. */
+    kind?: CoqFileProgressKind;
+}
+
+export interface CoqFileProgressParams {
+    /** The text document to which this progress notification applies. */
+    textDocument: VersionedTextDocumentIdentifier;
+
+    /**
+     * Array containing the parts of the file which are still being processed.
+     * The array should be empty if and only if the server is finished processing.
+     */
+    processing: CoqFileProgressProcessingInfo[];
+}
+
+export const coqFileProgress = new NotificationType<CoqFileProgressParams>('$/coq/fileProgress');
diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md
new file mode 100644
index 00000000..9f55d426
--- /dev/null
+++ b/etc/doc/PROTOCOL.md
@@ -0,0 +1,125 @@
+# coq-lsp protocol documentation
+
+## Introduction and preliminaries
+
+`coq-lsp` should be usable by standard LSP clients, however it
+implements some extensions tailored to improve Coq-specific use.
+
+As of today, this document is written for the 3.17 version of the LSP specification:
+https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification
+
+See also the upstream LSP issue on generic support for Proof
+Assistants
+https://github.com/microsoft/language-server-protocol/issues/1414
+
+## Language server protocol support table
+
+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`                      | No      | Planned                                                    |
+| `$/logTrace`                      | No      |                                                            |
+| `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`         | No      | Planned, blocked on upstream issues (#53)                  |
+| `textDocument/references`         | No      | Planned, blocked on upstream issues                        |
+| `textDocument/hover`              | Yes     |                                                            |
+| `textDocument/codeLens`           | No      |                                                            |
+| `textDocument/foldingRange`       | No      |                                                            |
+| `textDocument/documentSymbol`     | Yes     | Needs more work as to provide better results               |
+| `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      |                                                            |
+|-----------------------------------|---------|------------------------------------------------------------|
+
+
+## Extensions to the LSP specification
+
+As of today, `coq-lsp` implements two extensions to the LSP spec. Note
+that none of them are stable yet:
+
+### Goal Display
+
+In order to display proof goals, `coq-lsp` supports the `proof/goals` request, parameters are:
+```typescript
+{ textDocument: uri
+, position: Position
+}
+```
+
+Answer to the request is a `Goal[]` object, where
+```typescript
+interface Hyp {
+    names: string;
+    ty: string;
+}
+interface Goal {
+    ty: string;
+    hyps: Hyp[];
+}
+
+interface CoqFileProgressParams {
+
+```
+
+which can be then rendered by the client in way that is desired.
+
+`proof/goals` was first used in the lambdapi-lsp server implementation, and we adapted it.
+
+#### Changelog
+
+- v1: initial version, imported from lambdapi-lsp
+
+### File checking progress
+
+The `$/coq/fileProgress` notification is sent from server to client to
+describe the ranges of the document that have been processed.
+
+It is modelled after `$/lean/fileProgress`, see
+https://github.com/microsoft/language-server-protocol/issues/1414 for more information.
+
+```typescript
+enum CoqFileProgressKind {
+    Processing = 1,
+    FatalError = 2
+}
+
+interface CoqFileProgressProcessingInfo {
+    /** Range for which the processing info was reported. */
+    range: Range;
+    /** Kind of progress that was reported. */
+    kind?: CoqFileProgressKind;
+}
+
+interface CoqFileProgressParams {
+    /** The text document to which this progress notification applies. */
+    textDocument: VersionedTextDocumentIdentifier;
+
+    /**
+     * Array containing the parts of the file which are still being processed.
+     * The array should be empty if and only if the server is finished processing.
+     */
+    processing: CoqFileProgressProcessingInfo[];
+}
+```
+
+#### Changelog
+
+- v1: exact copy from Lean protocol (spec under Apache License)
diff --git a/fleche/debug.ml b/fleche/debug.ml
index 122ea085..fa59161f 100644
--- a/fleche/debug.ml
+++ b/fleche/debug.ml
@@ -16,3 +16,6 @@ let parsing = false || all
 
 (* Backtraces *)
 let backtraces = false || all
+
+(* Sched wakeup *)
+let sched_wakeup = false || all
diff --git a/fleche/doc.ml b/fleche/doc.ml
index 50797c7d..5c9124fe 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -7,9 +7,6 @@
 (* Status: Experimental                                                 *)
 (************************************************************************)
 
-(* open Lsp_util
- * module LSP = Lsp.Base *)
-
 let hd_opt ~default l =
   match l with
   | [] -> default
@@ -27,8 +24,8 @@ type node =
 
 module Completion = struct
   type t =
-    | Yes
-    | Stopped of Loc.t (* Location of the last valid token *)
+    | Yes of Loc.t  (** Location of the last token in the document *)
+    | Stopped of Loc.t  (** Location of the last valid token *)
 end
 
 (* Private. A doc is a list of nodes for now. The first element in the list is
@@ -38,6 +35,7 @@ type t =
   { uri : string
   ; version : int
   ; contents : string
+  ; end_loc : int * int * int
   ; root : Coq.State.t
   ; nodes : node list
   ; diags_dirty : bool  (** Used to optimize `eager_diagnostics` *)
@@ -51,9 +49,16 @@ let mk_doc root_state workspace =
 
 let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri })
 
+let get_last_text text =
+  let lines = CString.split_on_char '\n' text in
+  let last_line = hd_opt ~default:"" (List.rev lines) in
+  (List.length lines, String.length last_line, String.length text)
+
 let create ~state ~workspace ~uri ~version ~contents =
+  let end_loc = get_last_text contents in
   { uri
   ; contents
+  ; end_loc
   ; version
   ; root = mk_doc state workspace
   ; nodes = []
@@ -61,12 +66,14 @@ let create ~state ~workspace ~uri ~version ~contents =
   ; completed = Stopped (init_loc ~uri)
   }
 
-let bump_version ~version ~text doc =
+let bump_version ~version ~contents doc =
+  let end_loc = get_last_text contents in
   (* We need to resume checking in full when a new document *)
   { doc with
     version
   ; nodes = []
-  ; contents = text
+  ; contents
+  ; end_loc
   ; diags_dirty = false
   ; completed = Stopped (init_loc ~uri:doc.uri)
   }
@@ -89,6 +96,34 @@ let send_eager_diagnostics ~uri ~version ~doc =
 
 let set_completion ~completed doc = { doc with completed }
 
+(* We approximate the remnants of the document. It would be easier if instead of
+   reporting what is missing, we would report what is done, but for now we are
+   trying this paradigm.
+
+   As we are quite dynamic (for now) in terms of what we observe of the document
+   (basically we observe it linearly), we must compute the final position with a
+   bit of a hack. *)
+let compute_progress end_loc last_done =
+  let start =
+    { Types.Point.line = last_done.Loc.line_nb_last - 1
+    ; character = last_done.ep - last_done.bol_pos_last
+    ; offset = last_done.ep
+    }
+  in
+  let end_line, end_col, end_offset = end_loc in
+  let end_ =
+    { Types.Point.line = end_line - 1
+    ; character = end_col
+    ; offset = end_offset
+    }
+  in
+  let range = Types.Range.{ start; end_ } in
+  (range, 1)
+
+let report_progress ~doc last_tok =
+  let progress = compute_progress doc.end_loc last_tok in
+  Io.Report.fileProgress ~uri:doc.uri ~version:doc.version [ progress ]
+
 (* XXX: Save on close? *)
 (* let close_doc _modname = () *)
 
@@ -119,7 +154,6 @@ let parse_to_terminator : unit Pcoq.Entry.t =
 (* If an error occurred while parsing, we try to read the input until a dot
    token is encountered. We assume that when a lexer error occurs, at least one
    char was eaten *)
-
 let rec discard_to_dot ps =
   try Pcoq.Entry.parse parse_to_terminator ps with
   | CLexer.Error.E _ -> discard_to_dot ps
@@ -217,6 +251,7 @@ let build_span start_loc end_loc =
 let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
   let rec stm doc st last_tok =
     let doc = send_eager_diagnostics ~uri ~version ~doc in
+    report_progress ~doc last_tok;
     if Debug.parsing then Io.Log.error "coq" "parsing sentence";
     (* Parsing *)
     let action, parsing_diags, parsing_time =
@@ -225,7 +260,12 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
       | Coq.Protect.R.Interrupted, time -> (EOF (Stopped last_tok), [], time)
       | Coq.Protect.R.Completed res, time -> (
         match res with
-        | Ok None -> (EOF Yes, [], time)
+        | Ok None ->
+          (* We actually need to fix Coq to return the location of the true file
+             EOF, the below trick doesn't work. That will involved updating the
+             type of `main_entry` *)
+          let last_tok = Pcoq.Parsable.loc doc_handle in
+          (EOF (Yes last_tok), [], time)
         | Ok (Some ast) ->
           let () = if Debug.parsing then debug_parsed_sentence ~ast in
           (Process ast, [], time)
@@ -342,7 +382,7 @@ let log_resume last_tok =
 
 let check ~ofmt:_ ~doc ~fb_queue =
   match doc.completed with
-  | Yes ->
+  | Yes _ ->
     Io.Log.error "check" "resuming, completed=yes, nothing to do";
     doc
   | Stopped last_tok ->
@@ -369,11 +409,14 @@ let check ~ofmt:_ ~doc ~fb_queue =
        reverse the accumulators *)
     let doc = { doc with nodes = List.rev doc.nodes; contents } in
     let end_msg =
-      match doc.completed with
-      | Yes ->
-        "done: document fully checked "
-        ^ Pp.string_of_ppcmds (Loc.pr (Pcoq.Parsable.loc handle))
-      | Stopped loc -> "done: stopped at " ^ Pp.string_of_ppcmds (Loc.pr loc)
+      let timestamp = Unix.gettimeofday () in
+      let loc =
+        match doc.completed with
+        | Yes loc -> loc
+        | Stopped loc -> loc
+      in
+      Format.asprintf "done [%.2f]: document fully checked %a" timestamp
+        Pp.pp_with (Loc.pr loc)
     in
     Io.Log.error "check" end_msg;
     print_stats ();
diff --git a/fleche/doc.mli b/fleche/doc.mli
index 37c5da7a..4ade283a 100644
--- a/fleche/doc.mli
+++ b/fleche/doc.mli
@@ -28,14 +28,15 @@ type node =
 
 module Completion : sig
   type t =
-    | Yes
-    | Stopped of Loc.t (* Location of the last valid token *)
+    | Yes of Loc.t  (** Location of the last token in the document *)
+    | Stopped of Loc.t  (** Location of the last valid token *)
 end
 
 type t = private
   { uri : string
   ; version : int
   ; contents : string
+  ; end_loc : int * int * int
   ; root : Coq.State.t
   ; nodes : node list
   ; diags_dirty : bool
@@ -50,7 +51,7 @@ val create :
   -> contents:string
   -> t
 
-val bump_version : version:int -> text:string -> t -> t
+val bump_version : version:int -> contents:string -> t -> t
 
 val check :
   ofmt:Format.formatter -> doc:t -> fb_queue:Coq.Message.t list ref -> t
diff --git a/fleche/io.ml b/fleche/io.ml
index 63d3869b..25cce5ea 100644
--- a/fleche/io.ml
+++ b/fleche/io.ml
@@ -3,11 +3,14 @@ module CallBack = struct
     { log_error : string -> string -> unit
     ; send_diagnostics :
         uri:string -> version:int -> Types.Diagnostic.t list -> unit
+    ; send_fileProgress :
+        uri:string -> version:int -> (Types.Range.t * int) list -> unit
     }
 
   let default =
     { log_error = (fun _ _ -> ())
     ; send_diagnostics = (fun ~uri:_ ~version:_ _ -> ())
+    ; send_fileProgress = (fun ~uri:_ ~version:_ _ -> ())
     }
 
   let cb = ref default
@@ -21,4 +24,7 @@ end
 module Report = struct
   let diagnostics ~uri ~version d =
     !CallBack.cb.send_diagnostics ~uri ~version d
+
+  let fileProgress ~uri ~version d =
+    !CallBack.cb.send_fileProgress ~uri ~version d
 end
diff --git a/fleche/io.mli b/fleche/io.mli
index 338d91b9..0c0ab67a 100644
--- a/fleche/io.mli
+++ b/fleche/io.mli
@@ -3,6 +3,8 @@ module CallBack : sig
     { log_error : string -> string -> unit
     ; send_diagnostics :
         uri:string -> version:int -> Types.Diagnostic.t list -> unit
+    ; send_fileProgress :
+        uri:string -> version:int -> (Types.Range.t * int) list -> unit
     }
 
   val set : t -> unit
@@ -14,4 +16,7 @@ end
 
 module Report : sig
   val diagnostics : uri:string -> version:int -> Types.Diagnostic.t list -> unit
+
+  val fileProgress :
+    uri:string -> version:int -> (Types.Range.t * int) list -> unit
 end