From 65084c3e0ad04f6ba1b2997310d226070da9b6b9 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 11 Dec 2024 11:32:55 +0100 Subject: [PATCH 1/2] feat: the cursor is placed at the end of the error when block on error is active Until now, the cursor remained at the last correctly executed sentence. --- language-server/dm/documentManager.ml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index bf777dbc..a3b42714 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -285,17 +285,14 @@ let state_before_error state error_id = 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 match Document.find_sentence_before state.document start with | None -> - let start = Position.{line=0; character=0} in - let end_ = Position.{line=0; character=0} in - let last_range = Range.{start; end_} in let observe_id = Top in - {state with observe_id}, Some last_range + {state with observe_id}, Some error_range | Some { id } -> - let last_range = Document.range_of_id_with_blank_space state.document id in let observe_id = (Id id) in - {state with observe_id}, Some last_range + {state with observe_id}, Some error_range let observe ~background state id ~should_block_on_error : (state * event Sel.Event.t list) = match Document.get_sentence state.document id with @@ -313,8 +310,8 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve | None -> {state with execution_state}, [] | Some error_id -> - let state, last_range = state_before_error state error_id in - let events = mk_block_on_error_event last_range error_id in + let state, error_range = state_before_error state error_id in + let events = mk_block_on_error_event error_range error_id in {state with execution_state}, events let reset_to_top st = { st with observe_id = Top } @@ -533,8 +530,9 @@ 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, last_range = state_before_error st error_id in - let events = if block then mk_block_on_error_event last_range error_id else [] in + | Some error_id -> + let st, error_range = state_before_error st error_id in + let events = if block then mk_block_on_error_event error_range error_id else [] in st, events in let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in From e8f07ab817202588ca26fbb1a5e8e17c0685efb3 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 11 Dec 2024 14:44:10 +0100 Subject: [PATCH 2/2] feat: when possible, place the cursor at the end of the error range Sometimes the error range does not span the whole line. In that case, place the cursor at the end of the error range not the line. --- language-server/dm/documentManager.ml | 14 ++++++++------ language-server/dm/executionManager.ml | 8 ++++---- language-server/dm/executionManager.mli | 4 ++-- 3 files changed, 14 insertions(+), 12 deletions(-) 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