Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[parser] use the loc of the prev sentence to feed the parser #824

Merged
merged 2 commits into from
Jul 23, 2024
Merged

[parser] use the loc of the prev sentence to feed the parser #824

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
baf2df7
[parser] use the loc of the prev sentence to feed the parser
gares Jul 10, 2024
aea118f
comment
gares Jul 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 9 additions & 8 deletions language-server/dm/document.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -342,19 +342,20 @@ 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
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);
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
Expand All @@ -377,7 +378,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
Expand Down
Loading