From baf2df704663f1d06f4c37521df7bfbec7f2fdb4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Jul 2024 13:08:39 +0200 Subject: [PATCH 1/2] [parser] use the loc of the prev sentence to feed the parser In this way the line number in the loc is not reset to 0. This has no use internally, since the document holds the text and computes line number correctly, but Coq code and plugins may want to display a loc (with a correct line number) --- language-server/dm/document.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 0dd9a9310..bfaf0b545 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -291,18 +291,18 @@ let parse_one_sentence stream ~st = [%%if coq = "8.18" || coq = "8.19"] -let parse_one_sentence stream ~st = +let parse_one_sentence ?loc stream ~st = Vernacstate.Synterp.unfreeze st; let entry = Pvernac.main_entry (Some (Synterp.get_default_proof_mode ())) in - let pa = Pcoq.Parsable.make stream in + let pa = Pcoq.Parsable.make ?loc stream in let sentence = Pcoq.Entry.parse entry pa in (sentence, []) [%%else] -let parse_one_sentence stream ~st = +let parse_one_sentence ?loc stream ~st = Vernacstate.Synterp.unfreeze st; Flags.record_comments := true; let entry = Pvernac.main_entry (Some (Synterp.get_default_proof_mode ())) in - let pa = Pcoq.Parsable.make stream in + let pa = Pcoq.Parsable.make ?loc stream in let sentence = Pcoq.Entry.parse entry pa in let comments = Pcoq.Parsable.comments pa in (sentence, comments) @@ -342,7 +342,7 @@ let get_entry ast = [%%endif] -let rec parse_more synterp_state stream raw parsed parsed_comments errors = +let rec parse_more ?loc synterp_state stream raw parsed parsed_comments errors = let handle_parse_error start msg qf = log @@ "handling parse error at " ^ string_of_int start; let stop = Stream.count stream in @@ -354,7 +354,7 @@ let rec parse_more synterp_state stream raw parsed parsed_comments errors = log @@ "Start of parse is: " ^ (string_of_int start); begin (* FIXME should we save lexer state? *) - match parse_one_sentence stream ~st:synterp_state with + match parse_one_sentence ?loc stream ~st:synterp_state with | None, _ (* EOI *) -> List.rev parsed, errors, List.rev parsed_comments | Some ast, comments -> let stop = Stream.count stream in @@ -377,7 +377,7 @@ let rec parse_more synterp_state stream raw parsed parsed_comments errors = let parsed = sentence :: parsed in let comments = List.map (fun ((start, stop), content) -> {start; stop; content}) comments in let parsed_comments = List.append comments parsed_comments in - parse_more synterp_state stream raw parsed parsed_comments errors + parse_more ?loc:ast.loc synterp_state stream raw parsed parsed_comments errors with exn -> let e, info = Exninfo.capture exn in let loc = get_loc_from_info_or_exn e info in From aea118fbe0251100486ba5e64a051cda0fa81d01 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Jul 2024 13:27:53 +0200 Subject: [PATCH 2/2] comment --- language-server/dm/document.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index bfaf0b545..892483b5a 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -348,7 +348,8 @@ let rec parse_more ?loc synterp_state stream raw parsed parsed_comments errors = let stop = Stream.count stream in let parsing_error = { msg; start; stop; qf} in let errors = parsing_error :: errors in - parse_more synterp_state stream raw parsed parsed_comments errors + (* TODO: we could count the \n between start and stop and increase Loc.line_nb *) + parse_more ?loc synterp_state stream raw parsed parsed_comments errors in let start = Stream.count stream in log @@ "Start of parse is: " ^ (string_of_int start);