Skip to content

Commit

Permalink
Fix observe id invalidation bug
Browse files Browse the repository at this point in the history
This bug made navigation sometimes fail in manual mode.
  • Loading branch information
maximedenes committed Nov 21, 2023
1 parent a8dec86 commit baf0f6e
Show file tree
Hide file tree
Showing 2 changed files with 33 additions and 6 deletions.
16 changes: 10 additions & 6 deletions language-server/dm/documentManager.ml
Original file line number Diff line number Diff line change
Expand Up @@ -211,17 +211,21 @@ let interpret_in_background st =
| None -> (st, [])
| Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:true st id

let is_above st id1 id2 =
let range1 = Document.range_of_id st id1 in
let range2 = Document.range_of_id st id2 in
Position.compare range1.start range2.start < 0

let validate_document state =
let unchanged_id, invalid_ids, document = Document.validate_document state.document in
let update_observe_id id =
if Stateid.Set.mem id invalid_ids then unchanged_id
else Some id
let unchanged_id, invalid_roots, document = Document.validate_document state.document in
let observe_id = match unchanged_id, state.observe_id with
| None, _ | _, None -> None
| Some id, Some id' -> if is_above state.document id id' then Some id else Some id'
in
let observe_id = Option.bind state.observe_id update_observe_id in
let execution_state =
List.fold_left (fun st id ->
ExecutionManager.invalidate (Document.schedule state.document) id st
) state.execution_state (Stateid.Set.elements invalid_ids) in
) state.execution_state (Stateid.Set.elements invalid_roots) in
{ state with document; execution_state; observe_id }

let init init_vs ~opts uri ~text =
Expand Down
23 changes: 23 additions & 0 deletions language-server/tests/dm_tests.ml
Original file line number Diff line number Diff line change
Expand Up @@ -357,3 +357,26 @@ let%test_unit "edit.shift_error_before_sentence" =
let warning = Stdlib.List.hd @@ DocumentManager.all_diagnostics st in
[%test_eq: int] 41 (warning.range.start.character);
[%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, (s1, (s2, ())) = dm_parse st (P(P O)) in
let st, events = DocumentManager.interpret_to_end st 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 = 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, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in
let st, events = DocumentManager.interpret_to_end st 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 = 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))
(Some (Stateid.to_int s1.id))

0 comments on commit baf0f6e

Please sign in to comment.