coqdoc does not report the filename on errors

[charguer]

Description of the problem

When coqdoc is executed on multiple files, it does not report the filename from which the error comes from.
E.g.:

Line 1047, character 162, warning: unterminated "]"

I suspect the lines:

  let coq_file f m =
    reset ();
    let c = open_in f in
    let lb = from_channel c in
    let lb = { lb with lex_start_p = { lb.lex_start_p with pos_fname = f } } in

are insufficient because they don't update the pos_fname of lex_curr_p.

In OCaml 4.11, the following function was added:

let set_filename lexbuf fname =
  lexbuf.lex_curr_p <- {lexbuf.lex_curr_p with pos_fname = fname}

It probably suggests that we should set pos_fname for lex_curr_p, not (just) for lex_start_p.

Coq Version

All versions.

[herbelin]

Hi @charguer, thanks for the diagnosis. Documentation in OCaml's lexing.mli indeed says "Position tracking mode works as follows. At each token, the lexing engine will copy [lex_curr_p] to [lex_start_p]", so setting the latter is short-lived.

Implemented at #14285.