Merge pull request #805 from coq-community/fix-highlights

Fix highlights

Author: rtetley

language-server/dm/document.ml

@@ -227,16 +227,24 @@ let pos_at_end parsed =
   | Some (stop, _) -> stop
   | None -> -1
 
+let string_of_parsed_ast { tokens } = 
+  (* TODO implement printer for vernac_entry *)
+  "[" ^ String.concat "--" (List.map (Tok.extract_string false) tokens) ^ "]"
+
 let patch_sentence parsed scheduler_state_before id ({ parsing_start; ast; start; stop; synterp_state } : pre_sentence) =
-  log @@ "Patching sentence " ^ Stateid.to_string id;
   let old_sentence = SM.find id parsed.sentences_by_id in
+  log @@ Format.sprintf "Patching sentence %s , %s" (Stateid.to_string id) (string_of_parsed_ast old_sentence.ast);
   let scheduler_state_after, schedule =
     let ast = (ast.ast, ast.classification, synterp_state) in
     Scheduler.schedule_sentence (id,ast) scheduler_state_before parsed.schedule
   in
   let new_sentence = { old_sentence with ast; parsing_start; start; stop; scheduler_state_before; scheduler_state_after } in
   let sentences_by_id = SM.add id new_sentence parsed.sentences_by_id in
-  let sentences_by_end = LM.remove old_sentence.stop parsed.sentences_by_end in
+  let sentences_by_end = match LM.find_opt old_sentence.stop parsed.sentences_by_end with
+  | Some { id } when Stateid.equal id new_sentence.id ->
+    LM.remove old_sentence.stop parsed.sentences_by_end 
+  | _ -> parsed.sentences_by_end
+  in
   let sentences_by_end = LM.add new_sentence.stop new_sentence sentences_by_end in
   { parsed with sentences_by_end; sentences_by_id; schedule }, scheduler_state_after
 
@@ -245,9 +253,11 @@ type diff =
   | Added of pre_sentence list
   | Equal of (sentence_id * pre_sentence) list
 
+
+
 let same_tokens (s1 : sentence) (s2 : pre_sentence) =
     CList.equal Tok.equal s1.ast.tokens s2.ast.tokens
-
+  
 (* TODO improve diff strategy (insertions,etc) *)
 let rec diff old_sentences new_sentences =
   match old_sentences, new_sentences with
@@ -256,13 +266,10 @@ let rec diff old_sentences new_sentences =
   | old_sentences, [] -> [Deleted (List.map (fun s -> s.id) old_sentences)]
     (* FIXME something special should be done when `Deleted` is applied to a parsing effect *)
   | old_sentence::old_sentences, new_sentence::new_sentences ->
-    if same_tokens old_sentence new_sentence then
+    if same_tokens old_sentence new_sentence then 
       Equal [(old_sentence.id,new_sentence)] :: diff old_sentences new_sentences
-    else Deleted [old_sentence.id] :: Added [new_sentence] :: diff old_sentences new_sentences
-
-let string_of_parsed_ast { tokens } = 
-  (* TODO implement printer for vernac_entry *)
-  "[" ^ String.concat "--" (List.map (Tok.extract_string false) tokens) ^ "]" 
+    else 
+      Deleted [old_sentence.id] :: Added [new_sentence] :: diff old_sentences new_sentences
 
 let string_of_diff_item doc = function
   | Deleted ids ->
@@ -434,6 +441,13 @@ let invalidate top_edit top_id parsed_doc new_sentences =
       invalidate_diff parsed_doc scheduler_state invalid_ids diffs
   in
   let (_,_synterp_state,scheduler_state) = state_at_pos parsed_doc top_edit in
+  let sentence_strings = LM.bindings @@ LM.map (fun s -> string_of_parsed_ast s.ast) parsed_doc.sentences_by_end in
+  let sentence_strings = List.map (fun s -> snd s) sentence_strings in
+  let sentence_string = String.concat " " sentence_strings in
+  let sentence_strings_id = SM.bindings @@ SM.map (fun s -> string_of_parsed_ast s.ast) parsed_doc.sentences_by_id in
+  let sentence_strings_id = List.map (fun s -> snd s) sentence_strings_id in
+  let sentence_string_id = String.concat " " sentence_strings_id in
+  log @@ Format.sprintf "Top edit: %i, Doc: %s, Doc by id: %s" top_edit sentence_string sentence_string_id;
   let old_sentences = sentences_after parsed_doc top_edit in
   let diff = diff old_sentences new_sentences in
   let unchanged_id = unchanged_id top_id diff in

language-server/dm/document.mli

@@ -49,7 +49,9 @@ type parsing_error = {
 val parse_errors : document -> parsing_error list
 (** [parse_errors doc] returns the list of sentences which failed to parse
     (see validate_document) together with their error message *)
-
+val apply_text_edit : document -> text_edit -> document
+(** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new
+    text is not parsed or executed. *)
 val apply_text_edits : document -> text_edit list -> document
 (** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new
     text is not parsed or executed. *)

language-server/dm/documentManager.ml

@@ -368,15 +368,19 @@ let reset { uri; opts; init_vs; document; execution_state; observe_id } =
   validate_document st, [inject_em_event feedback]
 
 let apply_text_edits state edits =
-  let document = Document.apply_text_edits state.document edits in
-  let shift_diagnostics_locs exec_st (range, new_text) =
+  let apply_edit_and_shift_diagnostics_locs_and_overview state (range, new_text as edit) =
+    let document = Document.apply_text_edit state.document edit in
+    let exec_st = state.execution_state in
+    log @@ Format.sprintf "APPLYING TEXT EDIT %s [%s]" (Range.to_string range) new_text;
     let edit_start = RawDocument.loc_of_position (Document.raw_document state.document) range.Range.start in
     let edit_stop = RawDocument.loc_of_position (Document.raw_document state.document) range.Range.end_ in
     let edit_length = edit_stop - edit_start in
-    ExecutionManager.shift_diagnostics_locs exec_st ~start:edit_stop ~offset:(String.length new_text - edit_length)
+    let exec_st = ExecutionManager.shift_diagnostics_locs exec_st ~start:edit_stop ~offset:(String.length new_text - edit_length) in
+    let execution_state = ExecutionManager.shift_overview exec_st ~before:(Document.raw_document state.document) ~after:(Document.raw_document document) ~start:edit_stop ~offset:(String.length new_text - edit_length) in
+    {state with execution_state; document}
   in
-  let execution_state = List.fold_left shift_diagnostics_locs state.execution_state edits in
-  validate_document { state with document; execution_state }
+  let state = List.fold_left apply_edit_and_shift_diagnostics_locs_and_overview state edits in
+  validate_document state
 
 let handle_event ev st =
   match ev with

language-server/dm/executionManager.ml

@@ -756,6 +756,24 @@ let feedback st id =
 let all_feedback st =
   List.fold_left (fun acc (id, (_,l)) -> List.map (fun x -> (id, x)) l @ acc) [] @@ SM.bindings st.of_sentence
 
+let shift_overview st ~before ~after ~start ~offset =
+  let shift_loc loc_start loc_end =
+    if loc_start >= start then (loc_start + offset, loc_end + offset)
+    else if loc_end > start then (loc_start, loc_end + offset)
+    else (loc_start, loc_end)
+  in
+  let shift_range range =
+    let r_start = RawDocument.loc_of_position before range.Range.start in
+    let r_stop = RawDocument.loc_of_position before range.Range.end_ in
+    let r_start', r_stop' = shift_loc r_start r_stop in
+    Range.create ~start:(RawDocument.position_of_loc after r_start') ~end_:(RawDocument.position_of_loc after r_stop')
+  in
+  let processed = CList.Smart.map shift_range st.overview.processed in
+  let processing = CList.Smart.map shift_range st.overview.processing in
+  let prepared = CList.Smart.map shift_range st.overview.prepared in
+  let overview = {processed; processing; prepared} in
+  {st with overview}
+
 let shift_diagnostics_locs st ~start ~offset =
   let shift_loc loc =
     let (loc_start, loc_stop) = Loc.unloc loc in

language-server/dm/executionManager.mli

@@ -54,6 +54,7 @@ val feedback :  state -> sentence_id -> feedback_message list
 val all_errors : state -> (sentence_id * (Loc.t option * Pp.t * Quickfix.t list option)) list
 val all_feedback : state -> (sentence_id * feedback_message) list
 
+val shift_overview : state -> before:RawDocument.t -> after:RawDocument.t -> start:int -> offset:int -> state
 val shift_diagnostics_locs : state -> start:int -> offset:int -> state
 val executed_ids : state -> sentence_id list
 val is_executed : state -> sentence_id -> bool

language-server/tests/common.ml

@@ -124,12 +124,12 @@ let task st id spec =
 
 
 let rec handle_events n (events : DocumentManager.event Sel.Todo.t) st =
-  if n <= 0 then (Stdlib.Format.eprintf "handle_events run out of steps:\nTodo = %a\n" (Sel.Todo.pp DocumentManager.pp_event) events; Caml.exit 1)
+  if n <= 0 then (Stdlib.Format.eprintf "handle_events run out of steps:\nTodo = %a\n" (Sel.Todo.pp DocumentManager.pp_event) events; Stdlib.exit 1)
   else if Sel.Todo.is_empty events then st
 
   else begin
     (*Stdlib.Format.eprintf "waiting %a\n%!" Sel.(pp_todo DocumentManager.pp_event) events;*)
-    Caml.flush_all ();
+    Stdlib.flush_all ();
     let (ready, remaining) = Sel.pop_timeout ~stop_after_being_idle_for:0.1 events in
     match ready with
     | None -> 
@@ -164,7 +164,7 @@ let check_diag st specl =
     (range, message, severity) in
   let match_diagnostic r s rex (range, message, severity) =
     Range.included ~in_:r range &&
-    Caml.(=) severity (Some s) &&
+    Stdlib.(=) severity (Some s) &&
     Str.string_match (Str.regexp rex) message 0
   in
   let diagnostics = DocumentManager.all_diagnostics st in