Merge pull request #963 from coq/error-cursor-position

Place the cursor at the end of the error when block on error mode is active

language-server/dm/documentManager.ml

@@ -281,21 +281,20 @@ 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 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 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
@@ -312,9 +311,9 @@ 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, last_range = state_before_error state error_id in
-        let events = mk_block_on_error_event last_range 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
 
 let reset_to_top st = { st with observe_id = Top }
@@ -553,8 +552,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, 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
     let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in

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

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