diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index a3b42714..7e85a8dc 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -281,11 +281,13 @@ let create_execution_event background event = let priority = if background then None else Some PriorityManager.execution in Sel.now ?priority event -let state_before_error state error_id = +let state_before_error state error_id loc = match Document.get_sentence state.document error_id with | None -> state, None | Some { start } -> - let error_range = Document.range_of_id_with_blank_space state.document error_id in + let errored_sentence_range = Document.range_of_id_with_blank_space state.document error_id in + let error_range = + Option.cata (fun loc -> RawDocument.range_of_loc (Document.raw_document state.document) loc) errored_sentence_range loc in match Document.find_sentence_before state.document start with | None -> let observe_id = Top in @@ -309,8 +311,8 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve match error_id with | None -> {state with execution_state}, [] - | Some error_id -> - let state, error_range = state_before_error state error_id in + | Some (error_id, loc) -> + let state, error_range = state_before_error state error_id loc in let events = mk_block_on_error_event error_range error_id in {state with execution_state}, events @@ -530,8 +532,8 @@ let execute st id vst_for_next_todo started task background block = let st, block_events = match exec_error with | None -> st, [] - | Some error_id -> - let st, error_range = state_before_error st error_id in + | Some (error_id, loc) -> + let st, error_range = state_before_error st error_id loc in let events = if block then mk_block_on_error_event error_range error_id else [] in st, events in diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index f61c898d..f5f816e6 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -30,7 +30,7 @@ let error loc qf msg vernac_st = Error ((loc,msg), qf, (Some vernac_st)) type sentence_id = Stateid.t -type errored_sentence = sentence_id option +type errored_sentence = (sentence_id * Loc.t option) option module SM = Map.Make (Stateid) @@ -594,7 +594,7 @@ let execute_task st (vs, events, interrupted) task = let vs, v, ev = interp_ast ~doc_id:st.doc_id ~state_id:id ~st:vs ~error_recovery ast in let exec_error = match v with | Success _ -> None - | Error _ -> Some id + | Error ((loc, _), _, _) -> Some (id, loc) in let st = update st id v in (st, vs, events @ ev, false, exec_error) @@ -673,10 +673,10 @@ let build_tasks_for document sch st id block = (* We reached an already computed state *) log @@ "Reached computed state " ^ Stateid.to_string id; vs, tasks, st, None - | Some (Error(_,_,Some vs)) -> + | Some (Error((loc, _),_,Some vs)) -> (* We try to be resilient to an error *) log @@ "Error resiliency on state " ^ Stateid.to_string id; - vs, tasks, st, Some id + vs, tasks, st, Some (id, loc) | _ -> log @@ "Non (locally) computed state " ^ Stateid.to_string id; let (base_id, task) = task_for_sentence sch id in diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli index ceb2ebaf..c0bffea0 100644 --- a/language-server/dm/executionManager.mli +++ b/language-server/dm/executionManager.mli @@ -36,7 +36,7 @@ val is_diagnostics_enabled: unit -> bool type state type event type events = event Sel.Event.t list -type errored_sentence = sentence_id option +type errored_sentence = (sentence_id * Loc.t option) option type feedback_message = Feedback.level * Loc.t option * Quickfix.t list * Pp.t @@ -74,7 +74,7 @@ val handle_event : event -> state -> (sentence_id option * state option * events (** Execution happens in two steps. In particular the event one takes only one task at a time to ease checking for interruption *) type prepared_task -val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> bool -> Vernacstate.t * state * prepared_task option * sentence_id option +val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> bool -> Vernacstate.t * state * prepared_task option * errored_sentence val execute : state -> Document.document -> Vernacstate.t * events * bool -> prepared_task -> bool -> (prepared_task option * state * Vernacstate.t * events * errored_sentence) (* val update_overview : prepared_task -> prepared_task list -> state -> Document.document -> state