Skip to content

Commit

Permalink
[parser] use the loc of the prev sentence to feed the parser
Browse files Browse the repository at this point in the history
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)
  • Loading branch information
gares committed Jul 10, 2024
1 parent b64bef0 commit 6a4e82b
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions language-server/dm/document.ml
Original file line number Diff line number Diff line change
Expand Up @@ -290,18 +290,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 @@ -340,7 +340,7 @@ let get_entry ast =
Synterp.synterp_control ~intern 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 =
log @@ "handling parse error at " ^ string_of_int start;
let stop = Stream.count stream in
Expand All @@ -352,7 +352,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
Expand All @@ -375,7 +375,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 exn in
Expand Down

0 comments on commit 6a4e82b

Please # to comment.