From 3b4db9c01268fb327ed1d4b75d7eacc7c4fd644e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 Nov 2024 11:54:37 +0100 Subject: [PATCH] wip --- language-server/dm/document.ml | 3 + language-server/dm/document.mli | 1 + language-server/dm/documentManager.ml | 11 +- language-server/dm/documentManager.mli | 9 +- language-server/tests/common.ml | 63 ++++++-- language-server/tests/d_tests.ml | 35 ++-- language-server/tests/dm_tests.ml | 215 ++++++++++++------------- language-server/tests/em_tests.ml | 56 +++---- language-server/tests/goals.ml | 29 ++-- language-server/tests/s_tests.ml | 12 +- language-server/vscoqtop/lspManager.ml | 2 +- 11 files changed, 224 insertions(+), 212 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index fb7bded71..b129ea76c 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -109,6 +109,9 @@ type parse_state = { type event = | ParseEvent of parse_state | Invalidate of parse_state +let pp_event fmt = function + | ParseEvent _ -> Format.fprintf fmt "ParseEvent _" + | Invalidate _ -> Format.fprintf fmt "Invalidate _" type events = event Sel.Event.t list diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli index 23069000f..1b25df023 100644 --- a/language-server/dm/document.mli +++ b/language-server/dm/document.mli @@ -38,6 +38,7 @@ type outline_element = { type outline = outline_element list type event +val pp_event : Format.formatter -> event -> unit type events = event Sel.Event.t list diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index e15408fd8..733a1436f 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -433,7 +433,8 @@ let is_above st id1 id2 = let range2 = Document.range_of_id st id2 in Position.compare range1.start range2.start < 0 -let validate_document state unchanged_id invalid_roots document= +let validate_document state unchanged_id invalid_roots new_document = + (* BUG use state.document when parsing begun *) let observe_id = match unchanged_id, state.observe_id with | None, Id _ -> Top | _, Top -> Top @@ -443,7 +444,7 @@ let validate_document state unchanged_id invalid_roots document= List.fold_left (fun st id -> ExecutionManager.invalidate state.document (Document.schedule state.document) id st ) state.execution_state (Stateid.Set.elements invalid_roots) in - { state with document; execution_state; observe_id } + { state with document = new_document; execution_state; observe_id } [%%if coq = "8.18" || coq = "8.19"] let start_library top opts = Coqinit.start_library ~top opts @@ -561,7 +562,7 @@ let handle_execution_manager_event st ev = let update_view = true in {state=st; events=(inject_em_events events); update_view; notification=None} -let handle_event ev st block background diff_mode = +let handle_event ev st ~block ~background diff_mode = match ev with | Execute { id; vst_for_next_todo; started; task } -> execute st id vst_for_next_todo started task background block @@ -799,8 +800,7 @@ module Internal = struct | Top -> None | (Id id) -> Some id - let validate_document st = - validate_document st + let validate_document st (a,b,c) = validate_document st a b c let string_of_state st = let code_lines_by_id = Document.code_lines_sorted_by_loc st.document in @@ -820,5 +820,6 @@ module Internal = struct let string_by_id = String.concat "\n" @@ List.map string_of_item code_lines_by_id in let string_by_end = String.concat "\n" @@ List.map string_of_item code_lines_by_end in String.concat "\n" ["Document using sentences_by_id map\n"; string_by_id; "\nDocument using sentences_by_end map\n"; string_by_end] + let inject_doc_events = inject_doc_events end diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 6bac37bc8..42542778a 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -117,7 +117,7 @@ val get_proof : state -> Settings.Goals.Diff.Mode.t -> sentence_id option -> Pro val get_completions : state -> Position.t -> (completion_item list, string) Result.t -val handle_event : event -> state -> bool -> bool -> Settings.Goals.Diff.Mode.t -> handled_event +val handle_event : event -> state -> block:bool -> background:bool -> Settings.Goals.Diff.Mode.t -> handled_event (** handles events and returns a new state if it was updated. On top of the next events, it also returns info on whether execution has halted due to an error and returns a boolean flag stating whether the view should be updated *) @@ -145,12 +145,9 @@ module Internal : sig val execution_state : state -> ExecutionManager.state val string_of_state : state -> string val observe_id : state -> sentence_id option + val inject_doc_events : Document.event Sel.Event.t list -> event Sel.Event.t list - (* val validate_document : state -> state - (** [validate_document doc] reparses the text of [doc] and invalidates the - states impacted by the diff with the previously validated content. If the - text of [doc] has not changed since the last call to [validate_document], it - has no effect. *) *) + val validate_document : state -> sentence_id option * sentence_id_set * Document.document -> state end diff --git a/language-server/tests/common.ml b/language-server/tests/common.ml index b8d2b1002..dc615bfbf 100644 --- a/language-server/tests/common.ml +++ b/language-server/tests/common.ml @@ -37,7 +37,7 @@ let injections = let init_state = Vernacstate.freeze_full_state () let openDoc uri ~text = - DocumentManager.init init_state ~opts:injections uri ~text (Some DocumentManager.Top) + DocumentManager.init init_state ~opts:injections uri ~text let run r = [%test_pred: (_,string) Result.t ] (function Error _ -> false | _ -> true) r; @@ -72,7 +72,7 @@ let rec parse : type a. int -> int -> Document.sentence list -> Document.parsing | O, _, (_ :: _ as l) -> Error ("more errors than expected, extra " ^ Int.to_string (List.length l)) | P _, [], errors -> let errors = String.concat ~sep:"\n" @@ List.map ~f:(fun err -> snd err.Document.msg) errors in - Error ("fewer sentences than expected, only " ^ Int.to_string m ^ " list of errors:\n" ^ errors) + Error ("fewer sentences than expected, only " ^ Int.to_string m ^ " + errors:\n" ^ errors) | E _, _, [] -> Error ("fewer errors than expected, only " ^ Int.to_string n) let d_sentences doc spec = @@ -133,28 +133,48 @@ let task st id spec = init, run (task t spec) -let rec handle_events n (events : DocumentManager.event Sel.Todo.t) st = - if n <= 0 then (Stdlib.Format.eprintf "handle_events run out of steps:\nTodo = %a\n" (Sel.Todo.pp DocumentManager.pp_event) events; Stdlib.exit 1) - else if Sel.Todo.is_empty events then st +let rec handle_dm_events n (events : DocumentManager.event Sel.Todo.t) st = + if n <= 0 then (Stdlib.Format.eprintf "handle_dm_events run out of steps:\nTodo = %a\n" (Sel.Todo.pp DocumentManager.pp_event) events; Stdlib.exit 1) + else if Sel.Todo.is_empty events then st, events else begin (*Stdlib.Format.eprintf "waiting %a\n%!" Sel.(pp_todo DocumentManager.pp_event) events;*) Stdlib.flush_all (); let (ready, remaining) = Sel.pop_timeout ~stop_after_being_idle_for:0.1 events in match ready with - | None -> - st + | None -> st, events | Some ev -> + (* Stdlib.Format.eprintf "handle_dm_events: handling %a\n" DocumentManager.pp_event ev; *) let st, new_events = - match DocumentManager.handle_event ev st false with - | None, events', _ -> st, events' - | Some st, events', _ -> st, events' + match DocumentManager.handle_event ev st ~block:false ~background:false Protocol.Settings.Goals.Diff.Mode.Off with + | { DocumentManager.state = None; events = events' } -> st, events' + | { DocumentManager.state = Some st; events = events' } -> st, events' in let todo = Sel.Todo.add remaining new_events in - handle_events (n-1) todo st + handle_dm_events (n-1) todo st end -let handle_events e st = handle_events 100 e st - + + +let rec handle_d_events n (events : Document.event Sel.Todo.t) (st : Document.document) : sentence_id option * sentence_id_set * Document.document = + if n <= 0 then (Stdlib.Format.eprintf "handle_d_events run out of steps:\nTodo = %a\n" (Sel.Todo.pp Document.pp_event) events; Stdlib.exit 1) + else if Sel.Todo.is_empty events then assert false + else begin + (*Stdlib.Format.eprintf "waiting %a\n%!" Sel.(pp_todo DocumentManager.pp_event) events;*) + Stdlib.flush_all (); + let (ready, remaining) = Sel.pop_timeout ~stop_after_being_idle_for:0.1 events in + match ready with + | None -> assert false + | Some ev -> + match Document.handle_event st ev with + | st, new_events, None -> + let todo = Sel.Todo.add remaining new_events in + handle_d_events (n-1) todo st + | _, events, Some update-> assert(Sel.Todo.is_empty (Sel.Todo.add remaining events)); update + + end +let handle_d_events e st = handle_d_events 100 e st + + type diag_spec = | D of sentence_id * Lsp.Types.DiagnosticSeverity.t * string @@ -197,3 +217,20 @@ let check_diag st specl = let test_uri = Lsp.Types.DocumentUri.of_path "foo.v" let init_test_doc ~text = openDoc test_uri ~text +let whole_init_and_parse_test_doc ~text = + let dm, _ = openDoc test_uri ~text in + let doc = DocumentManager.Internal.document dm in + let doc, events = Document.validate_document doc in + let todo = Sel.Todo.(add empty events) in + let update = handle_d_events todo doc in + DocumentManager.Internal.validate_document dm update, update + + let init_and_parse_test_doc ~text = snd @@ whole_init_and_parse_test_doc ~text + let dm_init_and_parse_test_doc ~text = fst @@ whole_init_and_parse_test_doc ~text + + let em_init_test_doc ~text = + let dm, init_events = openDoc test_uri ~text in + handle_dm_events 100 Sel.Todo.(add empty init_events) dm + +let handle_dm_events e st = fst @@ handle_dm_events 100 e st + \ No newline at end of file diff --git a/language-server/tests/d_tests.ml b/language-server/tests/d_tests.ml index 5abca70fb..6bbb2a76f 100644 --- a/language-server/tests/d_tests.ml +++ b/language-server/tests/d_tests.ml @@ -5,6 +5,11 @@ open Base [@@@warning "-27"] +let validate_document doc = + let doc, events = Document.validate_document doc in + let todo = Sel.Todo.add Sel.Todo.empty events in + handle_d_events todo doc + let trdeps doc s1 = (* This closure should be an API used in Schedule used by ExecutionManager *) let rec trclose f s = @@ -14,14 +19,12 @@ let trdeps doc s1 = trclose (Scheduler.dependents (Document.schedule doc)) (Stateid.Set.singleton s1.id) let %test_unit "document: invalidate top" = - let dm, _ = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in - let doc = DocumentManager.Internal.document dm in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid); let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in [%test_eq: sentence_id option] (Some s5.id) unchanged; let doc = Document.apply_text_edits doc [Document.range_of_id doc s1.id,"Definition x := 4."] in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = validate_document doc in let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in [%test_eq: sentence_id list] [s1.id] (Stateid.Set.elements invalid); [%test_eq: sentence_id option] None unchanged; @@ -37,14 +40,12 @@ let %test_unit "document: invalidate top" = () let %test_unit "document: invalidate proof" = - let dm, _ = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in - let doc = DocumentManager.Internal.document dm in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid); let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in [%test_eq: sentence_id option] (Some s5.id) unchanged; let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,"idtac."] in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = validate_document doc in let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in [%test_eq: sentence_id list] [s3.id] (Stateid.Set.elements invalid); [%test_eq: sentence_id option] (Some s2.id) unchanged; @@ -61,14 +62,12 @@ let %test_unit "document: invalidate proof" = let %test_unit "document: invalidate proof 2" = - let dm, _ = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in - let doc = DocumentManager.Internal.document dm in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid); let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in [%test_eq: sentence_id option] (Some s5.id) unchanged; let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,""] in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = validate_document doc in let r1,(r2,(r3,(r4,()))) = d_sentences doc (P(P(P(P(O))))) in [%test_eq: sentence_id list] [s3.id;s4.id;s5.id] (Stateid.Set.elements invalid); [%test_eq: sentence_id option] (Some s2.id) unchanged; @@ -76,27 +75,23 @@ let %test_unit "document: invalidate proof 2" = [%test_eq: sentence_id] s2.id r2.id let %test_unit "document: delete line" = - let dm, _ = init_test_doc ~text:"Definition x:= 3. Lemma foo : x = 3. Proof. reflexitivity. Qed." in - let doc = DocumentManager.Internal.document dm in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x:= 3. Lemma foo : x = 3. Proof. reflexitivity. Qed." in [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid); let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in let doc = Document.apply_text_edits doc [Document.range_of_id doc s5.id,""] in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = validate_document doc in let sentences_id = Stateid.Set.of_list (List.map (Document.sentences doc) ~f:(fun s -> s.id)) in [%test_pred: sentence_id] (fun x -> not (Stateid.Set.mem x sentences_id)) s5.id; () let %test_unit "document: expand sentence" = - let dm, _ = init_test_doc ~text:"Lemma foo : x = 3. M." in - let doc = DocumentManager.Internal.document dm in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Lemma foo : x = 3. M." in [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid); let s1,(s2,()) = d_sentences doc (P(P(O))) in let range = Document.range_of_id doc s2.id in let new_range = Lsp.Types.Range.{ start = range.end_; end_ = range.end_ } in let doc = Document.apply_text_edits doc [new_range,"foo."] in - let unchanged, invalid, doc = Document.validate_document doc in + let unchanged, invalid, doc = validate_document doc in let r1,(r2,()) = d_sentences doc (P(P(O))) in [%test_eq: sentence_id] s1.id r1.id; () \ No newline at end of file diff --git a/language-server/tests/dm_tests.ml b/language-server/tests/dm_tests.ml index 26146e5ac..a3fd1a7e5 100644 --- a/language-server/tests/dm_tests.ml +++ b/language-server/tests/dm_tests.ml @@ -14,6 +14,7 @@ open Base open Dm open Common +open Protocol [@@@warning "-27"] @@ -23,13 +24,21 @@ let edit_text st ~start ~stop ~text = let start = RawDocument.position_of_loc doc start in let end_ = RawDocument.position_of_loc doc stop in let range = Lsp.Types.Range.{ start; end_ } in - DocumentManager.apply_text_edits st [(range, text)] + let st, events = DocumentManager.apply_text_edits st [(range, text)] in + let todo = Sel.Todo.add Sel.Todo.empty events in + handle_dm_events todo st + + let apply_text_edits st l = + let st, events = DocumentManager.apply_text_edits st l in + let todo = Sel.Todo.add Sel.Todo.empty events in + handle_dm_events todo st + let insert_text st ~loc ~text = edit_text st ~start:loc ~stop:loc ~text let%test_unit "parse.init" = - let st, events = init_test_doc ~text:"Definition x := true. Definition y := false." in + let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := false." in 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 @@ -38,7 +47,7 @@ let%test_unit "parse.init" = check_no_diag st let%test_unit "parse.insert" = - let st, events = init_test_doc ~text:"Definition x := true. Definition y := false." in + let st, init_events = em_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 : Document.sentence) -> s.Document.start) sentences in @@ -46,7 +55,7 @@ let%test_unit "parse.insert" = check_no_diag st let%test_unit "parse.squash" = - let st, events = init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in + let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in let st = edit_text st ~start:20 ~stop:21 ~text:"" in let doc = DocumentManager.Internal.document st in let sentences = Document.sentences doc in @@ -57,7 +66,7 @@ let%test_unit "parse.squash" = [%test_eq: int] (List.length (Document.parse_errors doc)) 1 let%test_unit "parse.error_recovery" = - let st, events = init_test_doc ~text:"## . Definition x := true. !! . Definition y := false." in + let st, init_events = em_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 : Document.sentence) -> s.Document.start) sentences in @@ -65,43 +74,29 @@ let%test_unit "parse.error_recovery" = [%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 st, init_events = em_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 : Document.sentence) -> s.Document.start) sentences in [%test_eq: int list] start_positions [ 0; 35 ]; check_no_diag st -let%test_unit "parse.validate_errors_twice" = - let st, events = init_test_doc ~text:"Lemma a : True. Proof. idtac (fun x -> x). Qed." in - let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(E(P O)))) in - let todo = Sel.Todo.(add empty events) in - let st = handle_events todo st in - let st = DocumentManager.Internal.validate_document st in - let doc = DocumentManager.Internal.document st in - [%test_eq: int] (List.length (Document.parse_errors doc)) 1; - let st = DocumentManager.Internal.validate_document st in - let doc = DocumentManager.Internal.document st in - [%test_eq: int] (List.length (Document.parse_errors doc)) 1 - let%test_unit "parse.invalidate_before_module" = - let st, init_events = init_test_doc ~text:"Check nat. Module M := Nat." in + let st, init_events = em_init_test_doc ~text:"Check nat. Module M := Nat." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in check_no_diag st; let doc = DocumentManager.Internal.document st in - let st = DocumentManager.apply_text_edits st [Document.range_of_id doc s1.id,""] in + let st = apply_text_edits st [(Document.range_of_id doc s1.id, "")] in check_no_diag st let%test_unit "exec.init" = - let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := false." in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - let ranges = (DocumentManager.executed_ranges st).processed in + let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := false." in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in + let ranges = (DocumentManager.executed_ranges st Settings.Mode.Manual).processed in let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in [%test_eq: int list] positions [ 0 ]; let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.end_.character) ranges in @@ -109,78 +104,73 @@ let%test_unit "exec.init" = check_no_diag st let%test_unit "exec.require_error" = - let st, init_events = init_test_doc ~text:"Require fuhidkgjh. Definition x := true." in + let st, init_events = em_init_test_doc ~text:"Require fuhidkgjh. Definition x := true." in let st, (s1, (s2, ())) = dm_parse st (E(P O)) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - let ranges = (DocumentManager.executed_ranges st).processed in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in + let ranges = (DocumentManager.executed_ranges st Settings.Mode.Manual).processed in let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in [%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 + let st, init_events = em_init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let todo = Sel.Todo.(add empty init_events) in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st = handle_dm_events todo st in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st); let doc = DocumentManager.Internal.document st in - let st = DocumentManager.apply_text_edits st [Document.range_of_id doc s2.id,""] in + let st = apply_text_edits st [Document.range_of_id doc s2.id,""] in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s1.id)) (DocumentManager.Internal.observe_id st) let%test_unit "step_forward.expand_sentence_observe_id" = - let st, init_events = init_test_doc ~text:"Definition x := 3. P." in + let st, init_events = em_init_test_doc ~text:"Definition x := 3. P." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let todo = Sel.Todo.(add empty init_events) in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st = handle_dm_events todo st in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st); let doc = DocumentManager.Internal.document st in let range = Document.range_of_id doc s2.id in let new_range = Lsp.Types.Range.{ start = range.end_; end_ = range.end_ } in - let st = DocumentManager.apply_text_edits st [new_range,"bar."] in + let st = apply_text_edits st [new_range,"bar."] in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s1.id)) (DocumentManager.Internal.observe_id st) let%test_unit "step_forward.insert_space_after_sentence_observe_id" = - let st, init_events = init_test_doc ~text:"Definition x := 3. P." in + let st, init_events = em_init_test_doc ~text:"Definition x := 3. P." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let todo = Sel.Todo.(add empty init_events) in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st = handle_dm_events todo st in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st); let doc = DocumentManager.Internal.document st in let range = Document.range_of_id doc s2.id in let new_range = Lsp.Types.Range.{ start = range.end_; end_ = range.end_ } in - let st = DocumentManager.apply_text_edits st [new_range," "] in + let st = apply_text_edits st [new_range," "] in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st) let%test_unit "step_forward.proof_view" = - let st, init_events = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3." in + let st, init_events = em_init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let todo = Sel.Todo.(add empty init_events) in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in + let st = handle_dm_events todo st in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st = handle_dm_events todo st in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st); let data = DocumentManager.get_proof st Protocol.Settings.Goals.Diff.Mode.Off None in [%test_eq: bool] (Option.is_some data) true @@ -190,34 +180,33 @@ let%test_unit "step_forward.proof_view" = [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s1.id)) (DocumentManager.Internal.observe_id st) *) let%test_unit "step_forward.document_begin" = - let st, init_events = init_test_doc ~text:"(* Some comment *)\nLemma foo : x = 3." in + let st, init_events = em_init_test_doc ~text:"(* Some comment *)\nLemma foo : x = 3." in let st, (s1, ()) = dm_parse st (P O) in - let todo = Sel.Todo.(add empty init_events) in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s1.id)) (DocumentManager.Internal.observe_id st) let%test_unit "step_backward.document_begin" = - let st, init_events = init_test_doc ~text:"(* Some comment *)\nLemma foo : x = 3." in + let st, init_events = em_init_test_doc ~text:"(* Some comment *)\nLemma foo : x = 3." in let st, (s1, ()) = dm_parse st (P O) in - let todo = Sel.Todo.(add empty init_events) in - let st, events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in - let st = handle_events todo st in - let todo = Sel.Todo.(add empty events) in - let st, events, _ = DocumentManager.interpret_to_previous st in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in + let todo = Sel.Todo.(add init_events events) in + let st, events = DocumentManager.interpret_to_previous st ~check_mode:Settings.Mode.Manual in + let st = handle_dm_events todo st in [%test_eq: bool] (Option.is_none (DocumentManager.Internal.observe_id st)) true (* let%test_unit "exec.insert" = let st, events = init_test_doc ~text:"Definition x := true. Definition y := false." in - (* let st = handle_events events st in *) + (* let st = handle_dm_events events st in *) let st = DocumentManager.validate_document st in - let st, events, _ = DocumentManager.interpret_to_end st in + let st, events = DocumentManager.interpret_to_end st in let st = insert_text st ~loc:0 ~text:"Definition z := 0. " in let st = DocumentManager.validate_document st in - let st, events, _ = DocumentManager.interpret_to_end st in + let st, events = DocumentManager.interpret_to_end st in let ranges = (DocumentManager.executed_ranges st).processed in let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.char) ranges in check_no_diag st; @@ -225,12 +214,11 @@ let%test_unit "exec.insert" = *) let%test_unit "edit.shift_warning_in_sentence" = - let st, init_events = init_test_doc ~text:"#[deprecated(note = \"foo\", since = \"foo\")] Definition x := true. Definition y := x." in + let st, init_events = em_init_test_doc ~text:"#[deprecated(note = \"foo\", since = \"foo\")] Definition x := true. Definition y := x." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in check_diag st [ D (s2.id,Warning,".*deprecated.*") ]; @@ -240,7 +228,7 @@ let%test_unit "edit.shift_warning_in_sentence" = let doc = DocumentManager.Internal.document st in let start = (Document.range_of_id doc s2.id).start in let range = Lsp.Types.Range.{ start; end_ = start } in - let st = DocumentManager.apply_text_edits st [range," "] in + let st = apply_text_edits st [range," "] in check_diag st [ D (s2.id,Warning,".*deprecated.*") ]; @@ -249,12 +237,11 @@ let%test_unit "edit.shift_warning_in_sentence" = [%test_eq: int] 85 (warning.range.end_.character) let%test_unit "edit.shift_warning_before_sentence" = - let st, init_events = init_test_doc ~text:"#[deprecated(note = \"foo\", since = \"foo\")] Definition x := true. Definition y := x." in + let st, init_events = em_init_test_doc ~text:"#[deprecated(note = \"foo\", since = \"foo\")] Definition x := true. Definition y := x." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in check_diag st [ D (s2.id,Warning,".*deprecated.*") ]; @@ -270,12 +257,11 @@ let%test_unit "edit.shift_warning_before_sentence" = [%test_eq: int] 85 (warning.range.end_.character) let%test_unit "edit.shift_error_in_sentence" = - let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := z." in + let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := z." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in check_diag st [ D (s2.id,Error,".*z was not found.*") ]; @@ -285,7 +271,7 @@ let%test_unit "edit.shift_error_in_sentence" = let doc = DocumentManager.Internal.document st in let start = (Document.range_of_id doc s2.id).start in let range = Lsp.Types.Range.{ start; end_ = start } in - let st = DocumentManager.apply_text_edits st [range," "] in + let st = apply_text_edits st [range," "] in check_diag st [ D (s2.id,Error,".*z was not found.*") ]; @@ -294,12 +280,11 @@ let%test_unit "edit.shift_error_in_sentence" = [%test_eq: int] 42 (warning.range.end_.character) let%test_unit "edit.shift_error_before_sentence" = - let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := z." in + let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := z." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in check_diag st [ D (s2.id,Error,".*z was not found.*") ]; @@ -315,23 +300,21 @@ let%test_unit "edit.shift_error_before_sentence" = [%test_eq: int] 42 (warning.range.end_.character) let%test_unit "edit.edit_non_root_observe_id_top" = - let st, init_events = init_test_doc ~text:"Definition x := 1. Definition y := 2." in + let st, init_events = em_init_test_doc ~text:"Definition x := 1. Definition y := 2." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in let st = edit_text st ~start:0 ~stop:18 ~text:"Definition x := 3." in [%test_eq: bool] (ExecutionManager.is_executed (DocumentManager.Internal.execution_state st) s2.id) false; [%test_eq: int option] (Option.map ~f:Stateid.to_int (DocumentManager.Internal.observe_id st)) None let%test_unit "edit.edit_non_root_observe_id" = - let st, init_events = init_test_doc ~text:"Definition x := 1. Definition y := 2. Definition z := 3." in + let st, init_events = em_init_test_doc ~text:"Definition x := 1. Definition y := 2. Definition z := 3." in let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in - let st, events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in + let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add init_events events) in + let st = handle_dm_events todo st in let st = edit_text st ~start:19 ~stop:37 ~text:"Definition y := 4." in [%test_eq: bool] (ExecutionManager.is_executed (DocumentManager.Internal.execution_state st) s3.id) false; [%test_eq: int option] (Option.map ~f:Stateid.to_int (DocumentManager.Internal.observe_id st)) diff --git a/language-server/tests/em_tests.ml b/language-server/tests/em_tests.ml index 43bdd6f9e..c78a3dbc4 100644 --- a/language-server/tests/em_tests.ml +++ b/language-server/tests/em_tests.ml @@ -14,6 +14,7 @@ open Base open Dm open Common +open Protocol [@@@warning "-27"] @@ -21,36 +22,34 @@ let set_delegation_mode mode = ExecutionManager.(set_options { delegation_mode = mode; completion_options = { enable = false; unificationLimit = 100; algorithm = StructuredSplitUnification; atomicFactor = 5.; sizeFactor = 5. }; enableDiagnostics = true }) let%test_unit "exec: finished proof" = - let st, init_events = init_test_doc ~text:"Lemma x : True. trivial. Qed. Check x." in +Stdlib.Format.eprintf "HEHEHEHEHE\n%!"; + let st, events = em_init_test_doc ~text:"Lemma x : True. trivial. Qed. Check x." in let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(P(P O)))) in - let st, exec_events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in + let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add events exec_events) in + let st = handle_dm_events todo st in check_diag st [ D (s4.id,Information,".*True.*") ] let%test_unit "exec: finished proof skip" = - let st, init_events = init_test_doc ~text:"Lemma x : True. trivial. Qed. Check x." in + let st, events = em_init_test_doc ~text:"Lemma x : True. trivial. Qed. Check x." in let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(P(P O)))) in set_delegation_mode SkipProofs; - let st, exec_events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in + let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add events exec_events) in + let st = handle_dm_events todo st in check_diag st [ D (s4.id,Information,".*True.*") ]; ExecutionManager.set_default_options () let%test_unit "exec: unfinished proof" = - let st, init_events = init_test_doc ~text:"Lemma x : True. Qed. Check x." in + let st, events = em_init_test_doc ~text:"Lemma x : True. Qed. Check x." in let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in - let st, exec_events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in + let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add events exec_events) in + let st = handle_dm_events todo st in let errors = ExecutionManager.all_errors (DocumentManager.Internal.execution_state st) in [%test_eq: bool] true (1 = List.length errors); check_diag st [ @@ -61,13 +60,12 @@ let%test_unit "exec: unfinished proof" = ] let%test_unit "exec: unfinished proof skip" = - let st, init_events = init_test_doc ~text:"Lemma x : True. Qed. Check x." in + let st, events = em_init_test_doc ~text:"Lemma x : True. Qed. Check x." in let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in set_delegation_mode SkipProofs; - let st, exec_events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in + let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add events exec_events) in + let st = handle_dm_events todo st in check_diag st [ D (s2.id,Error,".*incomplete proof.*") ]; @@ -77,13 +75,12 @@ let%test_unit "exec: unfinished proof skip" = ExecutionManager.set_default_options () let%test_unit "exec: unfinished proof delegate" = - let st, init_events = init_test_doc ~text:"Lemma x : True. Qed. Check x." in + let st, events = em_init_test_doc ~text:"Lemma x : True. Qed. Check x." in let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in set_delegation_mode (DelegateProofsToWorkers { number_of_workers = 1 }); - let st, exec_events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in + let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add events exec_events) in + let st = handle_dm_events todo st in check_diag st [ D (s2.id,Error,".*incomplete proof.*") ]; @@ -94,12 +91,11 @@ let%test_unit "exec: unfinished proof delegate" = let%test_unit "exec: unstarted proof" = - let st, init_events = init_test_doc ~text:"Qed. Check nat." in + let st, events = em_init_test_doc ~text:"Qed. Check nat." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in - let st, exec_events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in + let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add events exec_events) in + let st = handle_dm_events todo st in check_diag st [ D (s1.id,Error,".*No proof-editing in progress.*"); ]; diff --git a/language-server/tests/goals.ml b/language-server/tests/goals.ml index 89c745a53..25e3cfd79 100644 --- a/language-server/tests/goals.ml +++ b/language-server/tests/goals.ml @@ -15,31 +15,30 @@ open Base open Dm open Common +open Protocol let%test_unit "goals: encoding after replay from top" = - let st, init_events = init_test_doc ~text:"Lemma foo : forall x y, x + y = y + x." in + let st = dm_init_and_parse_test_doc ~text:"Lemma foo : forall x y, x + y = y + x." in let st, (_s1, ()) = dm_parse st (P O) in - let st, exec_events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in - let st, exec_events, _ = DocumentManager.interpret_to_previous st in + let st, exec_events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in let todo = Sel.Todo.(add empty exec_events) in - let st = handle_events todo st in - let st, exec_events, _ = DocumentManager.interpret_to_next st ~should_block_on_error:false in + let st = handle_dm_events todo st in + let st, exec_events = DocumentManager.interpret_to_previous st ~check_mode:Settings.Mode.Manual in let todo = Sel.Todo.(add empty exec_events) in - let st = handle_events todo st in + let st = handle_dm_events todo st in + let st, exec_events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add empty exec_events) in + let st = handle_dm_events todo st in let proof = Stdlib.Option.get (DocumentManager.get_proof st Protocol.Settings.Goals.Diff.Mode.Off None) in - let messages = DocumentManager.get_messages st None in + let messages = DocumentManager.get_messages st (Option.value_exn @@ DocumentManager.Internal.observe_id st) in let _json = Protocol.ExtProtocol.Notification.Server.ProofViewParams.yojson_of_t { proof = Some proof; messages } in () let%test_unit "goals: proof is available after error" = - let st, init_events = init_test_doc ~text:"Lemma foo : False. easy." in + let st = dm_init_and_parse_test_doc ~text:"Lemma foo : False. easy." in let st, (_s1, (_s2, ())) = dm_parse st (P (P O)) in - let st, exec_events, _ = DocumentManager.interpret_to_end st ~should_block_on_error:false in - let todo = Sel.Todo.(add empty init_events) in - let todo = Sel.Todo.(add todo exec_events) in - let st = handle_events todo st in + let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in + let todo = Sel.Todo.(add empty exec_events) in + let st = handle_dm_events todo st in let proof = DocumentManager.get_proof st Protocol.Settings.Goals.Diff.Mode.Off None in [%test_eq: bool] true (Option.is_some proof) \ No newline at end of file diff --git a/language-server/tests/s_tests.ml b/language-server/tests/s_tests.ml index f0acb83bf..31dd5dcc2 100644 --- a/language-server/tests/s_tests.ml +++ b/language-server/tests/s_tests.ml @@ -21,7 +21,7 @@ open Types (* ********************************************************** *) let %test_unit "schedule: parse error in proof step becomes skipped" = - let st, _ = init_test_doc ~text:"Lemma a : True. Proof. idtac (fun x -> x). Qed." in + let st = dm_init_and_parse_test_doc ~text:"Lemma a : True. Proof. idtac (fun x -> x). Qed." in let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(E(P O)))) in let init, (o, (p1,()), t) = task st s4.id (Proof(S O)) in [%test_eq: sentence_id option] (Some s1.id) init; @@ -32,7 +32,7 @@ let %test_unit "schedule: parse error in proof step becomes skipped" = let %test_unit "schedule: no section no proof using" = - let st, _ = init_test_doc ~text:"Lemma a : True. Proof. idtac. Qed." in + let st = dm_init_and_parse_test_doc ~text:"Lemma a : True. Proof. idtac. Qed." in let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(P(P O)))) in let init, (o, (p1,(p2,())), t) = task st s4.id (Proof(S(S O))) in [%test_eq: sentence_id option] (Some s1.id) init; @@ -43,7 +43,7 @@ let %test_unit "schedule: no section no proof using" = () let %test_unit "schedule: transparent lemma" = - let st, _ = init_test_doc ~text:"Lemma a : True. Proof. idtac. Defined." in + let st = dm_init_and_parse_test_doc ~text:"Lemma a : True. Proof. idtac. Defined." in let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(P(P O)))) in let init, e = task st s4.id Exec in [%test_eq: sentence_id option] (Some s3.id) init; @@ -51,7 +51,7 @@ let %test_unit "schedule: transparent lemma" = () let %test_unit "schedule: section with proof using" = - let st, _ = init_test_doc ~text:"Section A. Variable x : Prop. Lemma a : True. Proof. idtac. Qed." in + let st = dm_init_and_parse_test_doc ~text:"Section A. Variable x : Prop. Lemma a : True. Proof. idtac. Qed." in let st, (s1, (s2, (s3, (s4, (s5, (s6, ())))))) = dm_parse st (P(P(P(P(P(P O)))))) in let init, q = task st s6.id Exec in [%test_eq: sentence_id option] (Some s5.id) init; @@ -59,7 +59,7 @@ let %test_unit "schedule: section with proof using" = () let %test_unit "schedule: section closed" = - let st, _ = init_test_doc ~text:"Section A. End A. Lemma a : True. Proof. idtac. Qed." in + let st = dm_init_and_parse_test_doc ~text:"Section A. End A. Lemma a : True. Proof. idtac. Qed." in let st, (s1, (s2, (s3, (s4, (s5, (s6, ())))))) = dm_parse st (P(P(P(P(P(P O)))))) in let init, (o, (p1,(p2,())), t) = task st s6.id (Proof(S(S O))) in [%test_eq: sentence_id option] (Some s3.id) init; @@ -70,7 +70,7 @@ let %test_unit "schedule: section closed" = () let %test_unit "schedule: empty proof" = - let st, _ = init_test_doc ~text:"Lemma a : True. Qed." in + let st = dm_init_and_parse_test_doc ~text:"Lemma a : True. Qed." in let st, (s1, (s2, ())) = dm_parse st (P(P O)) in let init, (o, (), t) = task st s2.id (Proof O) in [%test_eq: sentence_id option] (Some s1.id) init; diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index fb44f0617..dc3717803 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -640,7 +640,7 @@ let handle_event = function [] | Some { st; visible } -> let background = !check_mode = Settings.Mode.Continuous in - let handled_event = Dm.DocumentManager.handle_event e st !block_on_first_error background !diff_mode in + let handled_event = Dm.DocumentManager.handle_event e st ~block:!block_on_first_error ~background !diff_mode in let events = handled_event.events in begin match handled_event.state with | None -> ()