Skip to content

Commit

Permalink
feat: when possible, place the cursor at the end of the error range
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
rtetley committed Dec 11, 2024
1 parent 65084c3 commit e8f07ab
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 12 deletions.
14 changes: 8 additions & 6 deletions language-server/dm/documentManager.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions language-server/dm/executionManager.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions language-server/dm/executionManager.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down

0 comments on commit e8f07ab

Please sign in to comment.