diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index edda41a5f..12ebe4ff3 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -29,13 +29,20 @@ type parsed_ast = { } type pre_sentence = { + parsing_start : int; start : int; stop : int; synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *) ast : parsed_ast; } +(* Example: *) +(* " Check 3. " *) +(* ^ ^ ^---- end *) +(* | |------------ start *) +(* |---------------- parsing_start *) type sentence = { + parsing_start : int; start : int; stop : int; synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *) @@ -70,22 +77,32 @@ let range_of_sentence raw (sentence : sentence) = let end_ = RawDocument.position_of_loc raw sentence.stop in Range.{ start; end_ } +let range_of_sentence_with_blank_space raw (sentence : sentence) = + let start = RawDocument.position_of_loc raw sentence.parsing_start in + let end_ = RawDocument.position_of_loc raw sentence.stop in + Range.{ start; end_ } + let range_of_id document id = match SM.find_opt id document.sentences_by_id with | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id) | Some sentence -> range_of_sentence document.raw_doc sentence +let range_of_id_with_blank_space document id = + match SM.find_opt id document.sentences_by_id with + | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id) + | Some sentence -> range_of_sentence_with_blank_space document.raw_doc sentence + let parse_errors parsed = List.map snd (LM.bindings parsed.parsing_errors_by_end) -let add_sentence parsed start stop (ast: parsed_ast) synterp_state scheduler_state_before = +let add_sentence parsed parsing_start start stop (ast: parsed_ast) synterp_state scheduler_state_before = let id = Stateid.fresh () in let ast' = (ast.ast, ast.classification, synterp_state) in let scheduler_state_after, schedule = Scheduler.schedule_sentence (id, ast') scheduler_state_before parsed.schedule in (* FIXME may invalidate scheduler_state_XXX for following sentences -> propagate? *) - let sentence = { start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in + let sentence = { parsing_start; start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in { parsed with sentences_by_end = LM.add stop sentence parsed.sentences_by_end; sentences_by_id = SM.add id sentence parsed.sentences_by_id; schedule @@ -102,9 +119,36 @@ let remove_sentence parsed id = let sentences parsed = List.map snd @@ SM.bindings parsed.sentences_by_id + +type comment = { + start : int; + stop : int; +} + +type code_line = + | Sentence of sentence + | ParsingError of parsing_error + | Comment of comment + +let start_of_code_line = function + | Sentence { start = x } -> x + | ParsingError { start = x } -> x + | Comment { start = x } -> x + +let compare_code_line x y = + let s1 = start_of_code_line x in + let s2 = start_of_code_line y in + s1 - s2 + +let code_lines_sorted_by_loc parsed = + List.sort compare_code_line @@ List.concat [ + (List.map (fun (_,x) -> Sentence x) @@ SM.bindings parsed.sentences_by_id) ; + (List.map (fun (_,x) -> ParsingError x) @@ LM.bindings parsed.parsing_errors_by_end) ; + [] (* todo comments *) + ] let sentences_sorted_by_loc parsed = - List.sort (fun ({ start = s1 } : sentence) { start = s2 } -> s1 - s2) @@ List.map snd @@ SM.bindings parsed.sentences_by_id + List.sort (fun ({start = s1} : sentence) {start = s2} -> s1 - s2) @@ List.map snd @@ SM.bindings parsed.sentences_by_id let sentences_before parsed loc = let (before,ov,_after) = LM.split loc parsed.sentences_by_end in @@ -178,14 +222,14 @@ let pos_at_end parsed = | Some (stop, _) -> stop | None -> -1 -let patch_sentence parsed scheduler_state_before id ({ ast; start; stop; synterp_state } : pre_sentence) = +let patch_sentence parsed scheduler_state_before id ({ parsing_start; ast; start; stop; synterp_state } : pre_sentence) = log @@ "Patching sentence " ^ Stateid.to_string id; let old_sentence = SM.find id parsed.sentences_by_id in let scheduler_state_after, schedule = let ast = (ast.ast, ast.classification, synterp_state) in Scheduler.schedule_sentence (id,ast) scheduler_state_before parsed.schedule in - let new_sentence = { old_sentence with ast; start; stop; scheduler_state_before; scheduler_state_after } in + let new_sentence = { old_sentence with ast; parsing_start; start; stop; scheduler_state_before; scheduler_state_after } in let sentences_by_id = SM.add id new_sentence parsed.sentences_by_id in let sentences_by_end = LM.remove old_sentence.stop parsed.sentences_by_end in let sentences_by_end = LM.add new_sentence.stop new_sentence sentences_by_end in @@ -267,6 +311,7 @@ let rec parse_more synterp_state stream raw parsed errors = parse_more synterp_state stream raw parsed 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 @@ -288,7 +333,7 @@ let rec parse_more synterp_state stream raw parsed errors = let entry = Synterp.synterp_control ast in let classification = Vernac_classifier.classify_vernac ast in let synterp_state = Vernacstate.Synterp.freeze () in - let sentence = { ast = { ast = entry; classification; tokens }; start = begin_char; stop; synterp_state } in + let sentence = { parsing_start = start; ast = { ast = entry; classification; tokens }; start = begin_char; stop; synterp_state } in let parsed = sentence :: parsed in parse_more synterp_state stream raw parsed errors with exn -> @@ -304,6 +349,11 @@ let rec parse_more synterp_state stream raw parsed errors = let loc = Loc.get_loc @@ Exninfo.info exn in junk_sentence_end stream; handle_parse_error start (loc,CLexer.Error.to_string e) + | exception exn -> + let e, info = Exninfo.capture exn in + let loc = Loc.get_loc @@ info in + junk_sentence_end stream; + handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) end let parse_more synterp_state stream raw = @@ -331,8 +381,8 @@ let invalidate top_edit top_id parsed_doc new_sentences = invalidate_diff parsed_doc scheduler_state invalid_ids diffs | Added new_sentences :: diffs -> (* FIXME could have side effect on the following, unchanged sentences *) - let add_sentence (parsed_doc,scheduler_state) ({ start; stop; ast; synterp_state } : pre_sentence) = - add_sentence parsed_doc start stop ast synterp_state scheduler_state + let add_sentence (parsed_doc,scheduler_state) ({ parsing_start; start; stop; ast; synterp_state } : pre_sentence) = + add_sentence parsed_doc parsing_start start stop ast synterp_state scheduler_state in let parsed_doc, scheduler_state = List.fold_left add_sentence (parsed_doc,scheduler_state) new_sentences in invalidate_diff parsed_doc scheduler_state invalid_ids diffs @@ -361,7 +411,7 @@ let validate_document ({ parsed_loc; raw_doc; } as document) = log @@ Format.sprintf "%i new sentences" (List.length new_sentences); let unchanged_id, invalid_ids, document = invalidate (stop+1) top_id document new_sentences in let parsing_errors_by_end = - List.fold_left (fun acc error -> LM.add error.stop error acc) errors new_errors + List.fold_left (fun acc (error : parsing_error) -> LM.add error.stop error acc) errors new_errors in let parsed_loc = pos_at_end document in unchanged_id, invalid_ids, { document with parsed_loc; parsing_errors_by_end } @@ -394,4 +444,16 @@ module Internal = struct sentence.start sentence.stop + let string_of_error error = + let (_, str) = error.msg in + Format.sprintf "[parsing error] [%s] (%i -> %i)" + str + error.start + error.stop + + let string_of_item = function + | Sentence sentence -> string_of_sentence sentence + | Comment _ -> "(* comment *)" + | ParsingError error -> string_of_error error + end diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli index 0b9e69e18..1b0c1bfaa 100644 --- a/language-server/dm/document.mli +++ b/language-server/dm/document.mli @@ -53,7 +53,13 @@ val apply_text_edits : document -> text_edit list -> document (** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new text is not parsed or executed. *) +(* Example: *) +(* " Check 3. " *) +(* ^ ^ ^---- end *) +(* | |------------ start *) +(* |---------------- parsing_start *) type sentence = { + parsing_start : int; start : int; stop : int; synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *) @@ -63,7 +69,18 @@ type sentence = { id : sentence_id; } +type comment = { + start : int; + stop : int; +} + +type code_line = + | Sentence of sentence + | ParsingError of parsing_error + | Comment of comment + val sentences : document -> sentence list +val code_lines_sorted_by_loc : document -> code_line list val sentences_sorted_by_loc : document -> sentence list val get_sentence : document -> sentence_id -> sentence option @@ -90,9 +107,14 @@ val get_last_sentence : document -> sentence option val schedule : document -> Scheduler.schedule val range_of_id : document -> Stateid.t -> Range.t +(** [range_of_id doc id] returns a Range object coressponding to the sentence id given in argument *) + +val range_of_id_with_blank_space : document -> Stateid.t -> Range.t +(** [range_of_id_with_blank_space doc id] returns a Range object coressponding to the sentence id given in argument but with the white spaces before (until the previous sentence) *) module Internal : sig val string_of_sentence : sentence -> string + val string_of_item : code_line -> string end \ No newline at end of file diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 243cff627..04c42865f 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -66,27 +66,25 @@ type exec_overview = { processed : Range.t list; } -let merge_ranges doc (r1,l) r2 = - let loc1 = RawDocument.loc_of_position doc r1.Range.end_ in - let loc2 = RawDocument.loc_of_position doc r2.Range.start in - if RawDocument.only_whitespace_between doc (loc1+1) (loc2-1) then +let merge_adjacent_ranges (r1,l) r2 = + if Position.compare r1.Range.end_ r2.Range.start == 0 then Range.{ start = r1.Range.start; end_ = r2.Range.end_ }, l else r2, r1 :: l -let compress_sorted_ranges doc = function +let compress_sorted_ranges = function | [] -> [] | range :: tl -> - let r, l = List.fold_left (merge_ranges doc) (range,[]) tl in + let r, l = List.fold_left merge_adjacent_ranges (range,[]) tl in r :: l -let compress_ranges doc ranges = +let compress_ranges ranges = let ranges = List.sort (fun { Range.start = s1 } { Range.start = s2 } -> Position.compare s1 s2) ranges in - compress_sorted_ranges doc ranges + compress_sorted_ranges ranges let executed_ranges doc execution_state loc = let ranges_of l = - compress_ranges (Document.raw_document doc) @@ List.map (Document.range_of_id doc) l + compress_ranges @@ List.map (Document.range_of_id_with_blank_space doc) l in let ids_before_loc = List.map (fun s -> s.Document.id) @@ Document.sentences_before doc loc in let processed_ids = List.filter (fun x -> ExecutionManager.is_executed execution_state x || ExecutionManager.is_remotely_executed execution_state x) ids_before_loc in @@ -472,15 +470,19 @@ module Internal = struct validate_document st let string_of_state st = - let sentences = Document.sentences_sorted_by_loc st.document in + let code_lines = Document.code_lines_sorted_by_loc st.document in let string_of_state id = if ExecutionManager.is_executed st.execution_state id then "(executed)" else if ExecutionManager.is_remotely_executed st.execution_state id then "(executed in worker)" else "(not executed)" in - let string_of_sentence sentence = - Document.Internal.string_of_sentence sentence ^ " " ^ string_of_state sentence.id + let string_of_item item = + Document.Internal.string_of_item item ^ " " ^ + match item with + | Sentence { id } -> string_of_state id + | ParsingError _ -> "(error)" + | Comment _ -> "(comment)" in - String.concat "\n" @@ List.map string_of_sentence sentences + String.concat "\n" @@ List.map string_of_item code_lines end diff --git a/language-server/dm/rawDocument.ml b/language-server/dm/rawDocument.ml index 60bd57116..290bb3318 100644 --- a/language-server/dm/rawDocument.ml +++ b/language-server/dm/rawDocument.ml @@ -104,12 +104,3 @@ let apply_text_edit raw (Range.{start; end_}, editText) = let new_text = before ^ editText ^ after in (* FIXME avoid concatenation *) let new_lines = compute_lines new_text in (* FIXME compute this incrementally *) { text = new_text; lines = new_lines }, start - -let only_whitespace_between raw loc1 loc2 = - let res = ref true in - for i = loc1 to loc2 do - let code = Char.code raw.text.[i] in - if code <> 0x20 && code <> 0xD && code <> 0xA && code <> 0x9 - then res := false - done; - !res \ No newline at end of file diff --git a/language-server/dm/rawDocument.mli b/language-server/dm/rawDocument.mli index d44f092b0..9ab8b74cf 100644 --- a/language-server/dm/rawDocument.mli +++ b/language-server/dm/rawDocument.mli @@ -29,7 +29,3 @@ val word_at_position: t -> Position.t -> string option (** Applies a text edit, and returns start location *) val apply_text_edit : t -> text_edit -> t * int - -(** Tests if document text contains only whitespace between the two provided - locations, included *) -val only_whitespace_between : t -> int -> int -> bool \ No newline at end of file diff --git a/language-server/tests/common.ml b/language-server/tests/common.ml index 6d668e55d..0b7bbf7c5 100644 --- a/language-server/tests/common.ml +++ b/language-server/tests/common.ml @@ -65,7 +65,7 @@ let rec parse : type a. int -> int -> Document.sentence list -> Document.parsing Error ("fewer sentences than expected, only " ^ Int.to_string m ^ " list of errors:\n" ^ errors) | E _, _, [] -> Error ("fewer errors than expected, only " ^ Int.to_string n) -let d_sentences doc spec = +let d_sentences doc spec = let sentences = Document.sentences_sorted_by_loc doc in let errors = Document.parse_errors doc in let r = run (parse 0 0 sentences errors spec) in diff --git a/language-server/tests/dm_tests.ml b/language-server/tests/dm_tests.ml index b8d15cac1..6f340e100 100644 --- a/language-server/tests/dm_tests.ml +++ b/language-server/tests/dm_tests.ml @@ -33,7 +33,7 @@ let%test_unit "parse.init" = let doc = Document.raw_document @@ DocumentManager.Internal.document st in [%test_eq: int] (RawDocument.end_loc doc) 44; let sentences = Document.sentences @@ DocumentManager.Internal.document st in - let positions = Stdlib.List.map (fun s -> s.Document.start) sentences in + let positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in [%test_eq: int list] positions [ 0; 22 ]; check_no_diag st @@ -41,7 +41,7 @@ let%test_unit "parse.insert" = let st, events = init_test_doc ~text:"Definition x := true. Definition y := false." in let st = insert_text st ~loc:0 ~text:"Definition z := 0. " in let sentences = Document.sentences @@ DocumentManager.Internal.document st in - let positions = Stdlib.List.map (fun s -> s.Document.start) sentences in + let positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in [%test_eq: int list] positions [ 0; 19; 41 ]; check_no_diag st @@ -50,8 +50,8 @@ let%test_unit "parse.squash" = let st = edit_text st ~start:20 ~stop:21 ~text:"" in let doc = DocumentManager.Internal.document st in let sentences = Document.sentences doc in - let start_positions = Stdlib.List.map (fun s -> s.Document.start) sentences in - let stop_positions = Stdlib.List.map (fun s -> s.Document.stop) sentences in + let start_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in + let stop_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.stop) sentences in [%test_eq: int list] start_positions [ 44 ]; [%test_eq: int list] stop_positions [ 62 ]; [%test_eq: int] (List.length (Document.parse_errors doc)) 1 @@ -60,14 +60,14 @@ let%test_unit "parse.error_recovery" = let st, events = init_test_doc ~text:"## . Definition x := true. !! . Definition y := false." in let doc = DocumentManager.Internal.document st in let sentences = Document.sentences doc in - let start_positions = Stdlib.List.map (fun s -> s.Document.start) sentences in + let start_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in [%test_eq: int list] start_positions [ 5; 32 ]; [%test_eq: int] (List.length (Document.parse_errors doc)) 2 let%test_unit "parse.extensions" = let st, events = init_test_doc ~text:"Notation \"## x\" := x (at level 0). Definition f (x : nat) := ##xx." in let sentences = Document.sentences @@ DocumentManager.Internal.document st in - let start_positions = Stdlib.List.map (fun s -> s.Document.start) sentences in + let start_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in [%test_eq: int list] start_positions [ 0; 35 ]; check_no_diag st @@ -117,7 +117,7 @@ let%test_unit "exec.require_error" = let st = handle_events todo st in let ranges = (DocumentManager.executed_ranges st).processed in let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in - [%test_eq: int list] positions [ 19 ] + [%test_eq: int list] positions [ 18 ] let%test_unit "step_forward.delete_observe_id" = let st, init_events = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3." in