[fleche] update progress indicator correctly on End Of File

Fixes #445

CHANGES.md

@@ -26,6 +26,8 @@
    failed to create or update is still valid, but in the right failed
    state. This is a much needed API change for a lot of use cases
    (@ejgallego, #604)
+ - update progress indicator correctly on End Of File (@ejgallego,
+   #605, fixes #445)
 
 # coq-lsp 0.1.8: Trick-or-treat
 -------------------------------
@@ -107,7 +109,7 @@
    (@ejgallego, #438, reported by David Ilcinkas)
  - Fix "Error message browser becomes non-visible when there are many
    goals" by using a fixed-position separated error display (@TDiazT,
-   #445, fixes #441)
+   #455, fixes #441)
  - Message about workspace detection was printing the wrong file,
    (@ejgallego, #444, reported by Alex Sanchez-Stern)
  - Display the list of pending obligations in info panel (@ejgallego,

examples/comments_end.v

@@ -0,0 +1,13 @@
+Definition a := 3.
+
+(*
+
+
+    Boooo
+    Boooo
+    Boooo
+
+
+
+*)
+

fleche/doc.ml

@@ -627,16 +627,16 @@ let parse_action ~lines ~st last_tok doc_handle =
     match res with
     | 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` *)
+         EOF, the below trick seems to work tho. Coq fix involves updating the
+         type of `Pcoq.main_entry` *)
       let last_tok = Coq.Parsing.Parsable.loc doc_handle in
       let last_tok = Coq.Utils.to_range ~lines last_tok in
       (EOF (Yes last_tok), [], feedback, time)
     | Ok (Some ast) ->
       let () = if Debug.parsing then DDebug.parsed_sentence ~ast in
       (Process ast, [], feedback, time)
     | Error (Anomaly (_, msg)) | Error (User (None, msg)) ->
-      (* We don't have a better altenative :(, usually missing error loc here
+      (* We don't have a better alternative :(, usually missing error loc here
          means an anomaly, so we stop *)
       let err_range = last_tok in
       let parse_diags = [ Diags.make err_range 1 msg ] in
@@ -828,6 +828,8 @@ let process_and_parse ~io ~target ~uri ~version doc last_tok doc_handle =
       | Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc
       | Stop (completed, node) ->
         let doc = add_node ~node doc in
+        (* See #445 *)
+        report_progress ~io ~doc (Completion.range completed);
         set_completion ~completed doc
       | Continue { state; last_tok; node } ->
         let n_errors = CList.count Lang.Diagnostic.is_error node.Node.diags in