wip

language-server/dm/document.ml

@@ -109,6 +109,9 @@ type parse_state = {
 type event = 
 | ParseEvent of parse_state
 | Invalidate of parse_state
+let pp_event fmt = function
+ | ParseEvent _ -> Format.fprintf fmt "ParseEvent _"
+ | Invalidate _ -> Format.fprintf fmt "Invalidate _"
 
 type events = event Sel.Event.t list
 

language-server/dm/document.mli

@@ -38,6 +38,7 @@ type outline_element = {
 type outline = outline_element list
 
 type event
+val pp_event : Format.formatter -> event -> unit
 
 type events = event Sel.Event.t list
 

language-server/dm/documentManager.ml

@@ -433,7 +433,8 @@ let is_above st id1 id2 =
   let range2 = Document.range_of_id st id2 in
   Position.compare range1.start range2.start < 0
 
-let validate_document state unchanged_id invalid_roots document=
+let validate_document state unchanged_id invalid_roots new_document =
+  (* BUG use state.document when parsing begun *)
   let observe_id = match unchanged_id, state.observe_id with
     | None, Id _ -> Top
     | _, Top -> Top
@@ -443,7 +444,7 @@ let validate_document state unchanged_id invalid_roots document=
     List.fold_left (fun st id ->
       ExecutionManager.invalidate state.document (Document.schedule state.document) id st
       ) state.execution_state (Stateid.Set.elements invalid_roots) in
-  { state with document; execution_state; observe_id }
+  { state with document = new_document; execution_state; observe_id }
 
 [%%if coq = "8.18" || coq = "8.19"]
 let start_library top opts = Coqinit.start_library ~top opts
@@ -561,7 +562,7 @@ let handle_execution_manager_event st ev =
   let update_view = true in
   {state=st; events=(inject_em_events events); update_view; notification=None}
 
-let handle_event ev st block background diff_mode =
+let handle_event ev st ~block ~background diff_mode =
   match ev with
   | Execute { id; vst_for_next_todo; started; task } ->
     execute st id vst_for_next_todo started task background block
@@ -799,8 +800,7 @@ module Internal = struct
     | Top -> None
     | (Id id) -> Some id
 
-  let validate_document st =
-    validate_document st
+  let validate_document st (a,b,c) = validate_document st a b c
 
   let string_of_state st =
     let code_lines_by_id = Document.code_lines_sorted_by_loc st.document in
@@ -820,5 +820,6 @@ module Internal = struct
     let string_by_id = String.concat "\n" @@ List.map string_of_item code_lines_by_id in
     let string_by_end = String.concat "\n" @@ List.map string_of_item code_lines_by_end in
     String.concat "\n" ["Document using sentences_by_id map\n"; string_by_id; "\nDocument using sentences_by_end map\n"; string_by_end]
+    let inject_doc_events = inject_doc_events
 
 end

language-server/dm/documentManager.mli

@@ -117,7 +117,7 @@ val get_proof : state -> Settings.Goals.Diff.Mode.t -> sentence_id option -> Pro
 
 val get_completions : state -> Position.t -> (completion_item list, string) Result.t
 
-val handle_event : event -> state -> bool -> bool -> Settings.Goals.Diff.Mode.t -> handled_event
+val handle_event : event -> state -> block:bool -> background:bool -> Settings.Goals.Diff.Mode.t -> handled_event
 (** handles events and returns a new state if it was updated. On top of the next events, it also returns info
     on whether execution has halted due to an error and returns a boolean flag stating whether the view
     should be updated *)
@@ -145,12 +145,9 @@ module Internal : sig
   val execution_state : state -> ExecutionManager.state
   val string_of_state : state -> string
   val observe_id : state -> sentence_id option
+  val inject_doc_events : Document.event Sel.Event.t list -> event Sel.Event.t list
 
-  (* val validate_document : state -> state
-  (** [validate_document doc] reparses the text of [doc] and invalidates the
-      states impacted by the diff with the previously validated content. If the
-      text of [doc] has not changed since the last call to [validate_document], it
-      has no effect. *) *)
+  val validate_document : state -> sentence_id option * sentence_id_set * Document.document -> state
 
 
 end

language-server/tests/common.ml

@@ -37,7 +37,7 @@ let injections =
 let init_state = Vernacstate.freeze_full_state ()
 
 let openDoc uri ~text =
-  DocumentManager.init init_state ~opts:injections uri ~text (Some DocumentManager.Top)
+  DocumentManager.init init_state ~opts:injections uri ~text
 
 let run r =
   [%test_pred: (_,string) Result.t ] (function Error _ -> false | _ -> true) r;
@@ -72,7 +72,7 @@ let rec parse : type a. int -> int -> Document.sentence list -> Document.parsing
     | O, _, (_ :: _ as l) -> Error ("more errors than expected, extra " ^ Int.to_string (List.length l))
     | P _, [], errors ->
       let errors = String.concat ~sep:"\n" @@ List.map ~f:(fun err -> snd err.Document.msg) errors in
-      Error ("fewer sentences than expected, only " ^ Int.to_string m ^ " list of errors:\n" ^ errors)
+      Error ("fewer sentences than expected, only " ^ Int.to_string m ^ "  + errors:\n" ^ errors)
     | E _, _, [] -> Error ("fewer errors than expected, only " ^ Int.to_string n)
 
 let d_sentences doc spec =
@@ -133,28 +133,48 @@ let task st id spec =
   init, run (task t 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; Stdlib.exit 1)
-  else if Sel.Todo.is_empty events then st
+let rec handle_dm_events n (events : DocumentManager.event Sel.Todo.t) st =
+  if n <= 0 then (Stdlib.Format.eprintf "handle_dm_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, events
 
   else begin
     (*Stdlib.Format.eprintf "waiting %a\n%!" Sel.(pp_todo DocumentManager.pp_event) events;*)
     Stdlib.flush_all ();
     let (ready, remaining) = Sel.pop_timeout ~stop_after_being_idle_for:0.1 events in
     match ready with
-    | None -> 
-      st
+    | None -> st, events
     | Some ev ->
+      (* Stdlib.Format.eprintf "handle_dm_events: handling %a\n"  DocumentManager.pp_event ev; *)
       let st, new_events =
-        match DocumentManager.handle_event ev st false with
-        | None, events', _ -> st, events'
-        | Some st, events', _ -> st, events'
+        match DocumentManager.handle_event ev st ~block:false ~background:false Protocol.Settings.Goals.Diff.Mode.Off with
+        | { DocumentManager.state = None; events = events' } -> st, events'
+        | { DocumentManager.state = Some st; events = events' } -> st, events'
       in
       let todo = Sel.Todo.add remaining new_events in
-      handle_events (n-1) todo st
+      handle_dm_events (n-1) todo st
   end
-let handle_events e st = handle_events 100 e st
-
+
+
+let rec handle_d_events n (events : Document.event Sel.Todo.t) (st : Document.document) : sentence_id option * sentence_id_set * Document.document =
+  if n <= 0 then (Stdlib.Format.eprintf "handle_d_events run out of steps:\nTodo = %a\n" (Sel.Todo.pp Document.pp_event) events; Stdlib.exit 1)
+  else if Sel.Todo.is_empty events then assert false
+  else begin
+    (*Stdlib.Format.eprintf "waiting %a\n%!" Sel.(pp_todo DocumentManager.pp_event) events;*)
+    Stdlib.flush_all ();
+    let (ready, remaining) = Sel.pop_timeout ~stop_after_being_idle_for:0.1 events in
+    match ready with
+    | None -> assert false
+    | Some ev ->
+        match Document.handle_event st ev with
+        | st, new_events, None ->
+            let todo = Sel.Todo.add remaining new_events in
+            handle_d_events (n-1) todo st
+        | _, events, Some update-> assert(Sel.Todo.is_empty (Sel.Todo.add remaining events)); update
+
+  end
+let handle_d_events e st = handle_d_events 100 e st
+
+
 type diag_spec =
   | D of sentence_id * Lsp.Types.DiagnosticSeverity.t * string
 
@@ -197,3 +217,20 @@ let check_diag st specl =
 let test_uri = Lsp.Types.DocumentUri.of_path "foo.v"
 
 let init_test_doc ~text = openDoc test_uri ~text
+let whole_init_and_parse_test_doc ~text =
+  let dm, _ = openDoc test_uri ~text in
+  let doc = DocumentManager.Internal.document dm in
+  let doc, events = Document.validate_document doc in
+  let todo = Sel.Todo.(add empty events) in
+  let update = handle_d_events todo doc in
+  DocumentManager.Internal.validate_document dm update, update
+
+  let init_and_parse_test_doc ~text = snd @@ whole_init_and_parse_test_doc ~text
+  let dm_init_and_parse_test_doc ~text = fst @@ whole_init_and_parse_test_doc ~text
+
+  let em_init_test_doc ~text =
+    let dm, init_events = openDoc test_uri ~text in
+    handle_dm_events 100 Sel.Todo.(add empty init_events) dm
+
+let handle_dm_events e st = fst @@ handle_dm_events 100 e st
+

language-server/tests/d_tests.ml

@@ -5,6 +5,11 @@ open Base
 
 [@@@warning "-27"]
 
+let validate_document doc =
+  let doc, events = Document.validate_document doc in
+  let todo = Sel.Todo.add Sel.Todo.empty events in
+  handle_d_events todo doc
+
 let trdeps doc s1 =
   (* This closure should be an API used in Schedule used by ExecutionManager *)
   let rec trclose f s =
@@ -14,14 +19,12 @@ let trdeps doc s1 =
   trclose (Scheduler.dependents (Document.schedule doc)) (Stateid.Set.singleton s1.id)
 
 let %test_unit "document: invalidate top" =
-  let dm, _ = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
-  let doc = DocumentManager.Internal.document dm in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   [%test_eq: sentence_id option] (Some s5.id) unchanged;
   let doc = Document.apply_text_edits doc [Document.range_of_id doc s1.id,"Definition x := 4."] in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = validate_document doc in
   let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   [%test_eq: sentence_id list] [s1.id] (Stateid.Set.elements invalid);
   [%test_eq: sentence_id option] None unchanged;
@@ -37,14 +40,12 @@ let %test_unit "document: invalidate top" =
   ()
 
 let %test_unit "document: invalidate proof" =
-  let dm, _ = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
-  let doc = DocumentManager.Internal.document dm in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   [%test_eq: sentence_id option] (Some s5.id) unchanged;
   let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,"idtac."] in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = validate_document doc in
   let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   [%test_eq: sentence_id list] [s3.id] (Stateid.Set.elements invalid);
   [%test_eq: sentence_id option] (Some s2.id) unchanged;
@@ -61,42 +62,36 @@ let %test_unit "document: invalidate proof" =
 
 
 let %test_unit "document: invalidate proof 2" =
-  let dm, _ = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
-  let doc = DocumentManager.Internal.document dm in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   [%test_eq: sentence_id option] (Some s5.id) unchanged;
   let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,""] in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = validate_document doc in
   let r1,(r2,(r3,(r4,()))) = d_sentences doc (P(P(P(P(O))))) in
   [%test_eq: sentence_id list] [s3.id;s4.id;s5.id] (Stateid.Set.elements invalid);
   [%test_eq: sentence_id option] (Some s2.id) unchanged;
   [%test_eq: sentence_id] s1.id r1.id;
   [%test_eq: sentence_id] s2.id r2.id
 
 let %test_unit "document: delete line" = 
-  let dm, _ = init_test_doc ~text:"Definition x:= 3. Lemma foo : x = 3. Proof. reflexitivity. Qed." in 
-  let doc = DocumentManager.Internal.document dm in 
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Definition x:= 3. Lemma foo : x = 3. Proof. reflexitivity. Qed." in 
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
   let doc = Document.apply_text_edits doc [Document.range_of_id doc s5.id,""] in
-  let unchanged, invalid, doc = Document.validate_document doc in 
+  let unchanged, invalid, doc = validate_document doc in 
   let sentences_id = Stateid.Set.of_list (List.map (Document.sentences doc) ~f:(fun s -> s.id)) in
   [%test_pred: sentence_id] (fun x -> not (Stateid.Set.mem x sentences_id)) s5.id;
   ()
 
 let %test_unit "document: expand sentence" =
-  let dm, _ = init_test_doc ~text:"Lemma foo : x = 3. M." in
-  let doc = DocumentManager.Internal.document dm in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = init_and_parse_test_doc ~text:"Lemma foo : x = 3. M." in
   [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
   let s1,(s2,()) = d_sentences doc (P(P(O))) in
   let range = Document.range_of_id doc s2.id in
   let new_range = Lsp.Types.Range.{ start = range.end_; end_ = range.end_ } in
   let doc = Document.apply_text_edits doc [new_range,"foo."] in
-  let unchanged, invalid, doc = Document.validate_document doc in
+  let unchanged, invalid, doc = validate_document doc in
   let r1,(r2,()) = d_sentences doc (P(P(O))) in
   [%test_eq: sentence_id] s1.id r1.id;
   ()