Progress indicator and comments don't interact correctly

[Alizter]

The following has the "correct" progress indication:

Comments Here is some vernac.
Comments Here is some vernac.
Comments Here is some vernac.

Here is how it is rendered:

However adding a new line leaves a trailing "processing" indicator:

It always appears to be the last 2 lines:

Furthermore, commenting out the end lines will leave the progress indicator there too:

[ejgallego]

This is because Coq will actually not process that part of the file, there is already a TODO in doc.ml:

    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` *)
      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)

So indeed Coq's parser will eat the comment and then return None, giving us no info about the rest of the buffer.

The best way to fix this would be for the Coq parser to give us the last seen location in the file, that would involve modifying Pvernac.Vernac_.main_entry to have a better type:

    val main_entry : vernac_control option Entry.t

We could also change our code to infer the last location in the file from contents, however I'm a bit way of us doing that, as it would mask any strange stuff coming from Coq.