diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 70f0967e0..733a1436f 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -588,6 +588,8 @@ let handle_event ev st ~block ~background diff_mode = {state; events; update_view; notification=None} | Some (unchanged_id, invalid_roots, document) -> let st = validate_document st unchanged_id invalid_roots document in + let execution_state = ExecutionManager.reset_overview st.execution_state st.document in + let st = {st with execution_state} in let update_view = true in if background then let (st, events) = interpret_in_background st ~should_block_on_error:block in diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index d6d8814f9..49eca1e27 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -410,6 +410,20 @@ let update_overview task state document = | [] -> state | next :: _ -> update_processing next state document + +let build_prepared_overview state document = + List.fold_right (fun task st -> update_prepared task document st) state.todo state + +let build_processed_overview state document = + let sentence_ids = SM.bindings state.of_sentence in + let sentence_ids = List.map (fun x -> fst x) sentence_ids in + List.fold_right (fun id st -> update_processed id st document) sentence_ids state + +let reset_overview st document = + log "RESETTING OVERVIEW"; + let st = build_processed_overview st document in + build_prepared_overview st document + let prepare_overview st prepared = let overview = {st.overview with prepared} in {st with overview} @@ -832,8 +846,6 @@ let invalidate1 of_sentence id = let rec invalidate document schedule id st = log @@ "Invalidating: " ^ Stateid.to_string id; - let st = invalidate_processed id st document in - let st = invalidate_prepared_or_processing_sentence id st document in let of_sentence = invalidate1 st.of_sentence id in let old_jobs = Queue.copy jobs in let removed = ref [] in @@ -847,13 +859,6 @@ let rec invalidate document schedule id st = end) old_jobs; let of_sentence = List.fold_left invalidate1 of_sentence List.(concat (map (fun tasks -> map id_of_prepared_task tasks) !removed)) in - let rec invalidate_prepared_or_processing_tasks tasks st = - begin match tasks with - | [] -> st - | task :: l -> invalidate_prepared_or_processing_tasks l (invalidate_prepared_or_processing task st document) - end - in - let st = invalidate_prepared_or_processing_tasks (List.concat !removed) st in if of_sentence == st.of_sentence then st else let deps = Scheduler.dependents schedule id in Stateid.Set.fold (invalidate document schedule) deps { st with of_sentence } diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli index 87bdcdc47..4d03db89b 100644 --- a/language-server/dm/executionManager.mli +++ b/language-server/dm/executionManager.mli @@ -55,6 +55,7 @@ val feedback : state -> sentence_id -> feedback_message list val all_errors : state -> (sentence_id * (Loc.t option * Pp.t * Quickfix.t list option)) list val all_feedback : state -> (sentence_id * feedback_message) list +val reset_overview : state -> Document.document -> state val shift_overview : state -> before:RawDocument.t -> after:RawDocument.t -> start:int -> offset:int -> state val shift_diagnostics_locs : state -> start:int -> offset:int -> state val executed_ids : state -> sentence_id list