diff --git a/language-server/dm/scheduler.ml b/language-server/dm/scheduler.ml index c8733a70..b425c0b2 100644 --- a/language-server/dm/scheduler.ml +++ b/language-server/dm/scheduler.ml @@ -200,7 +200,7 @@ let push_state id ast synterp classif st = base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence end | VtQuery -> (* queries have no impact, we don't push them *) - base_id st, st, Query ex_sentence + base_id st, push_ex_sentence ex_sentence st, Query ex_sentence | VtProofStep _ -> base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence | VtSideff _ -> diff --git a/language-server/tests/dm_tests.ml b/language-server/tests/dm_tests.ml index 43c7b4ab..e6626b94 100644 --- a/language-server/tests/dm_tests.ml +++ b/language-server/tests/dm_tests.ml @@ -86,7 +86,6 @@ let%test_unit "parse.invalidate_before_module" = let st, events = DocumentManager.interpret_to_end st 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 = apply_text_edits st [(Document.range_of_id doc s1.id, "")] in check_no_diag st