Merge pull request #1014 from coq/continuous-mode-reg

Send a proof view in continuous mode when cursor position was executed

Author: rtetley

language-server/dm/documentManager.ml

@@ -554,6 +554,19 @@ let execution_finished st id started =
 
 let execute st id vst_for_next_todo started task background block =
   let time = Unix.gettimeofday () -. started in
+  let proof_view_event = (*When in continuous mode we always check if we should update the goal view *)
+    if background then begin
+      match st.observe_id with
+      | Top -> []
+      | Id o_id ->
+        let s_id = ExecutionManager.get_id_of_executed_task task in
+        if o_id = s_id then
+          [mk_proof_view_event s_id]
+        else []
+    end
+    else
+      []
+  in
   match Document.get_sentence st.document id with
   | None ->
     log (Printf.sprintf "ExecuteToLoc %d stops after %2.3f, sentences invalidated" (Stateid.to_int id) time);
@@ -578,7 +591,7 @@ let execute st id vst_for_next_todo started task background block =
         let event = Option.cata (fun event -> [event]) [] event in
         let state = Some {st with execution_state; cancel_handle} in
         let update_view = true in
-        let events = inject_em_events events @ block_events @ event in
+        let events = proof_view_event @ inject_em_events events @ block_events @ event in
         {state; events; update_view; notification=None}
 
 let get_proof st diff_mode id =

language-server/dm/executionManager.ml

@@ -97,6 +97,14 @@ type state = {
   overview: exec_overview;
 }
 
+let get_id_of_executed_task task =
+  match task with
+  | PSkip {id} -> id
+  | PBlock {id} -> id
+  | PExec {id} -> id
+  | PQuery {id} -> id
+  | PDelegate {terminator_id} -> terminator_id
+
 let print_exec_overview overview =
   let {processing; processed; prepared } = overview in
   log @@ "--------- Prepared ranges ---------";

language-server/dm/executionManager.mli

@@ -41,7 +41,6 @@ type errored_sentence = (sentence_id * Loc.t option) option
 type feedback_message = Feedback.level * Loc.t option * Quickfix.t list * Pp.t
 
 val pr_event : event -> Pp.t
-
 val init : Vernacstate.t -> state * event Sel.Event.t
 val destroy : state -> unit
 
@@ -74,6 +73,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 get_id_of_executed_task : prepared_task -> sentence_id
 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)