Parsing failure prevents from showing log messages in debug terminal

[Alidra]

In Vscode (and probably with Emacs too), when a proof is started but end is missing at the end of the proof, the console doesn't show the log messages except the last one which is Unexpected token: "". For instance, with the following file

verbose 3;
constant symbol T : TYPE;
opaque symbol trivial : T → T → T → T
≔ begin

The command line check command produces :

Checking "somefile.lp" ...
verbose 3
somefile.lp:2:0-25
symbol T : TYPE
[somefile.lp:5:7] Unexpected token: "".

But the Vscode Lambdapi debug terminal show only Unexpected token: "" (despite console 3; at the beginning of the file) and only when the end of file is reached.

[fblanqui]

Change proposal in lp_doc.ml:

let check_text ~doc =
  let uri, version = doc.uri, doc.version in
  let cmds, error = Pure.parse_text ~fname:uri doc.text in
  let root =
    match doc.root with
    | Some ss -> ss
    | None ->
        raise(Error.fatal_no_pos "Root state is missing probably because \
                                  new_doc raised an exception")
  in
  let nodes, final, diags, logs =
    List.fold_left (process_cmd uri) ([],root,[],[]) cmds in
  let logs = List.rev logs
  and diags = (* filter out diagnostics with no position *)
    List.fold_left (fun acc (pos,lvl,msg,goal) ->
        match pos with
        | None     -> acc
        | Some pos -> (pos,lvl,msg,goal) :: acc
      ) [] diags
  in
  let logs, diags =
    match error with
    | None -> logs, diags
    | Some(pos,msg) -> ((1, msg), Some pos)::logs, (pos,1,msg,None)::diags
  in
  let map = Pure.rangemap cmds in
  let doc = { doc with nodes; final=Some(final); map; logs } in
  doc, LSP.mk_diagnostics ~uri ~version diags

Changes in pure.ml: remove Parse_error exception and:

let parse_text :
      fname:string -> string -> Command.t list * (Pos.pos * string) option =
  fun ~fname s ->
  let parse_string =
    if Filename.check_suffix fname dk_src_extension then
      Parser.Dk.parse_string
    else Parser.parse_string
  in
  let cmds = Stdlib.ref [] in
  try
    Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) (parse_string fname s);
    List.rev Stdlib.(!cmds), None
  with
  | Fatal(Some(Some(pos)), msg) -> List.rev Stdlib.(!cmds), Some(pos, msg)
  | Fatal(Some(None)     , _  ) -> assert false
  | Fatal(None           , _  ) -> assert false

Change in pure.mli: remove Parse_error and

(** [parse_text ~fname contents] runs the parser on the string [contents] as
    if it were a file named [fname]. It returns the list of commands it could
    parse and, either [None] if it could parse all commands, or some position
    and error message otherwise. *)
val parse_text :
  fname:string -> string -> Command.t list * (Pos.pos * string) option

[Alidra]

Seems to work with theses modifications. However, if the end token is missing, you don't see an error message unless you add some tokens after the proof (for instance symbol B:TYPE;) in which case, the message Unexpected token: "symbol" is shown but not in the right place. But this shouldn't be hard to fix.

[Alidra]

So, we probably still need to show an error message if the user navigates to the end of the file

[fblanqui]

I cannot see that it works on my machine with

verbose 3;
symbol T : TYPE;
symbol trivial : T → T → T → T
≔ begin
  assume _ _ x;
  refine x;

nothing is printed in emacs or vscode despite verbose 3.

[Alidra]

Are you sure your are in the right branch? I just push more fixes (the parsing error is in the right place now) Can you check again please?