Updating document validation. Fixing observe_id when setting changes …

…to Continuous mode.

language-server/dm/documentManager.ml

@@ -171,14 +171,6 @@ let get_messages st pos =
     | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback
     | None -> feedback
 
-let reset { uri; opts; init_vs; document; execution_state } =
-  let text = RawDocument.text @@ Document.raw_document document in
-  Vernacstate.unfreeze_full_state init_vs;
-  let document = Document.create_document init_vs.synterp text in
-  ExecutionManager.destroy execution_state;
-  let execution_state, feedback = ExecutionManager.init init_vs in
-  { uri; opts; init_vs; document; execution_state; observe_id = None }, [inject_em_event feedback]
-
 let observe ~background state id : (state * event Sel.Event.t list) =
   match Document.get_sentence state.document id with
   | None -> (state, []) (* TODO error? *)
@@ -191,8 +183,10 @@ let observe ~background state id : (state * event Sel.Event.t list) =
       let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in
       (state, [ event ])
 
+let clear_observe_id st = 
+  { st with observe_id = None }
+
 let interpret_to st id =
-
   let observe_id = if st.observe_id = None then None else (Some (Id id)) in
   let st = { st with observe_id} in
   observe ~background:false st id
@@ -233,12 +227,12 @@ let interpret_to_next st =
       | Some {id } -> interpret_to st id
 
 let interpret_to_end st =
-  match Document.get_last_sentence st.document with 
+  match Document.get_last_sentence st.document with
   | None -> (st, [])
   | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to st id
 
 let interpret_in_background st =
-  match Document.get_last_sentence st.document with 
+  match Document.get_last_sentence st.document with
   | None -> (st, [])
   | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); observe ~background:true st id
 
@@ -251,16 +245,8 @@ let validate_document state =
   let unchanged_id, invalid_roots, document = Document.validate_document state.document in
   let observe_id = match unchanged_id, state.observe_id with
     | None, _ | _, None -> None
-    | Some id, Some id' -> if is_above state.document id id' then Some id else Some id'
-  in
-  let update_observe_id = function
-    | Top -> Some Top
-    | Id id ->
-      if Stateid.Set.mem id invalid_roots then 
-        match unchanged_id with
-        | None -> Some (Top)
-        | Some id -> Some (Id id)
-      else Some (Id id)
+    | _, Some Top -> Some Top
+    | Some id, Some (Id id') -> if is_above state.document id id' then Some (Id id) else state.observe_id
   in
   let execution_state =
     List.fold_left (fun st id ->
@@ -278,13 +264,14 @@ let init init_vs ~opts uri ~text observe_id =
   let st = { uri; opts; init_vs; document; execution_state; observe_id } in
   validate_document st, [inject_em_event feedback]
 
-let reset { uri; opts; init_vs; document; execution_state } =
+let reset { uri; opts; init_vs; document; execution_state; observe_id } =
   let text = RawDocument.text @@ Document.raw_document document in
   Vernacstate.unfreeze_full_state init_vs;
   let document = Document.create_document init_vs.synterp text in
   ExecutionManager.destroy execution_state;
   let execution_state, feedback = ExecutionManager.init init_vs in
-  let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in
+  let observe_id = if observe_id = None then None else (Some Top) in
+  let st = { uri; opts; init_vs; document; execution_state; observe_id} in
   validate_document st, [inject_em_event feedback]
 
 let apply_text_edits state edits =
@@ -384,7 +371,7 @@ let hover st pos =
   | Some pattern ->
     log ("hover: found word at cursor: " ^ pattern);
     let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
-    match get_context st pos with 
+    match get_context st pos with
     | None -> log "hover: no context found"; None
     | Some (sigma, env) ->
       try
@@ -421,7 +408,7 @@ let locate st pos ~pattern =
 
 let print st pos ~pattern = 
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
-  match get_context st pos with 
+  match get_context st pos with
   | None -> Error("No context found")
   | Some (sigma, env) -> 
     let qid = parse_entry st loc (Pcoq.Prim.smart_global) pattern in

language-server/dm/documentManager.mli

@@ -42,6 +42,9 @@ val apply_text_edits : state -> text_edit list -> state
     document is parsed, outdated executions states are invalidated, and the observe
     id is updated. *)
 
+val clear_observe_id : state -> state
+(** [clear_observe_id state] updates the state to make the observe_id None *)
+
 val interpret_to_position : state -> Position.t -> (state * events)
 (** [interpret_to_position stateful doc pos] navigates to the last sentence ending
     before or at [pos] and returns the resulting state. The [stateful] flag 

language-server/vscoqtop/lspManager.ml

@@ -206,7 +206,8 @@ let update_view uri st =
   )
 
 let run_documents () =
-  let interpret_doc_in_bg path st events =
+  let interpret_doc_in_bg path (st : Dm.DocumentManager.state) events =
+    let st = Dm.DocumentManager.clear_observe_id st in
     let (st, events') = Dm.DocumentManager.interpret_in_background st in
     let uri = DocumentUri.of_path path in
     Hashtbl.replace states path st;