diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 5d0ed2f22..12ebe4ff3 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -125,28 +125,31 @@ type comment = { stop : int; } -type item = +type code_line = | Sentence of sentence | ParsingError of parsing_error | Comment of comment -let start_of_item = function +let start_of_code_line = function | Sentence { start = x } -> x | ParsingError { start = x } -> x | Comment { start = x } -> x -let compare_item x y = - let s1 = start_of_item x in - let s2 = start_of_item y in +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 sentences_sorted_by_loc parsed = - List.sort compare_item @@ List.concat [ +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 + let sentences_before parsed loc = let (before,ov,_after) = LM.split loc parsed.sentences_by_end in let before = Option.cata (fun v -> LM.add loc v before) before ov in diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli index cb08386fe..1b0c1bfaa 100644 --- a/language-server/dm/document.mli +++ b/language-server/dm/document.mli @@ -74,13 +74,14 @@ type comment = { stop : int; } -type item = +type code_line = | Sentence of sentence | ParsingError of parsing_error | Comment of comment val sentences : document -> sentence list -val sentences_sorted_by_loc : document -> item 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 val sentences_before : document -> int -> sentence list @@ -114,6 +115,6 @@ val range_of_id_with_blank_space : document -> Stateid.t -> Range.t module Internal : sig val string_of_sentence : sentence -> string - val string_of_item : item -> 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 1f228bd68..04c42865f 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -470,7 +470,7 @@ 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)" @@ -483,6 +483,6 @@ module Internal = struct | ParsingError _ -> "(error)" | Comment _ -> "(comment)" in - String.concat "\n" @@ List.map string_of_item sentences + String.concat "\n" @@ List.map string_of_item code_lines end 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..b047df54a 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