Merge pull request #1001 from coq/push-query

Fix messages in contiunous mode
coq · Jan 22, 2025 · 084a980 · 084a980
2 parents 8333f37 + b68f425
commit 084a980
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git 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
@@ -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