fix: adapt to new api after rebase

Author: rtetley

language-server/dm/document.ml

@@ -107,7 +107,7 @@ type parse_state = {
   loc: Loc.t option;
   synterp_state : Vernacstate.Synterp.t;
   stream: (unit, char) Gramlib.Stream.t;
-  raw: RawDocument.t;
+  raw: RawDocument.t option;
   parsed: pre_sentence list;
   errors: parsing_error list;
   parsed_comments: comment list;
@@ -522,15 +522,15 @@ let handle_parse_error start msg qf ({stream; errors;} as parse_state) =
   let errors = parsing_error :: errors in
   let parse_state = {parse_state with errors} in
   (* TODO: we could count the \n between start and stop and increase Loc.line_nb *)
-  create_parsing_event (ParseEvent parse_state)
+  ParseEvent parse_state
 
 let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments} as parse_state) =
   let start = Stream.count stream in
   log @@ "Start of parse is: " ^ (string_of_int start);
   begin
     (* FIXME should we save lexer state? *)
     match parse_one_sentence ?loc stream ~st:synterp_state with
-    | None, _ (* EOI *) -> create_parsing_event (Invalidate parse_state)
+    | None, _ (* EOI *) -> Invalidate parse_state
     | Some ast, comments ->
       let stop = Stream.count stream in
       log @@ "Parsed: " ^ (Pp.string_of_ppcmds @@ Ppvernac.pr_vernac ast);
@@ -539,13 +539,14 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
               | Some lc -> lc.line_nb, lc.bp, lc.ep
               | None -> assert false
       in
-      let tokens = match raw with
-      | None -> []
-      | Some raw ->
-        let str = String.sub (RawDocument.text raw) begin_char (end_char - begin_char) in
-        let sstr = Stream.of_string str in
-        let lex = CLexer.Lexer.tok_func sstr in
-        stream_tok 0 [] lex begin_line begin_char in
+        let tokens = match raw with
+        | None -> []
+        | Some raw ->
+          let str = String.sub (RawDocument.text raw) begin_char (end_char - begin_char) in
+          let sstr = Stream.of_string str in
+          let lex = CLexer.Lexer.tok_func sstr in
+          stream_tok 0 [] lex begin_line begin_char 
+        in
       begin
         try
           let entry = get_entry ast in
@@ -557,7 +558,7 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
           let parsed_comments = List.append comments parsed_comments in
           let loc = ast.loc in
           let parse_state = {parse_state with parsed_comments; parsed; loc; synterp_state} in
-          create_parsing_event (ParseEvent parse_state)
+          ParseEvent parse_state
         with exn ->
           let e, info = Exninfo.capture exn in
           let loc = get_loc_from_info_or_exn e info in
@@ -639,7 +640,7 @@ let validate_document ({ parsed_loc; raw_doc; cancel_handle } as document) =
   while Stream.count stream < stop do Stream.junk () stream done;
   log @@ Format.sprintf "Parsing more from pos %i" stop;
   let started = Unix.gettimeofday () in
-  let parsed_state = {stop; top_id;synterp_state; stream; raw=raw_doc; parsed=[]; errors=[]; parsed_comments=[]; loc=None; started; previous_document=document} in
+  let parsed_state = {stop; top_id;synterp_state; stream; raw=(Some raw_doc); parsed=[]; errors=[]; parsed_comments=[]; loc=None; started; previous_document=document} in
   let priority = Some PriorityManager.parsing in
   let event = Sel.now ?priority (ParseEvent parsed_state) in
   let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
@@ -672,19 +673,29 @@ let handle_invalidate {parsed; errors; parsed_comments; stop; top_id; started; p
 let handle_event document = function
 | ParseEvent state -> 
   let event = handle_parse_more state in
+  let event = create_parsing_event event in
   let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
   {document with cancel_handle}, [event], None
 | Invalidate state -> {document with cancel_handle=None}, [], handle_invalidate state document
 
+let rec parse_full = function
+| ParseEvent state ->
+  let event = handle_parse_more state in
+  parse_full event
+| Invalidate state ->
+  state
+
 let parse_text_at_loc loc text document =
-  let (_, synterp_state, scheduler_state) = state_strictly_before document loc in
+  let top_id = Option.map (fun sentence -> sentence.id) (find_sentence_strictly_before document loc) in
+  let (stop, synterp_state, scheduler_state) = state_strictly_before document loc in
   let stream = Stream.of_string text in
-  let new_sentences, _ = parse_more synterp_state stream None in
+  let parsed_state = {synterp_state; started = Unix.gettimeofday (); top_id; stream; raw=None; loc=None; errors=[]; parsed=[]; parsed_comments=[]; previous_document=document; stop} in
+  let {parsed} = parse_full (ParseEvent parsed_state) in
   let add_sentence (sentences, schedule, scheduler_state) ({ parsing_start; start; stop; ast; synterp_state } : pre_sentence) =
     let added_sentence, schedule, schedule_state = pre_sentence_to_sentence parsing_start start stop ast synterp_state scheduler_state schedule in
     sentences @ [added_sentence], schedule, schedule_state
   in
-  let sentences, schedule, _ = List.fold_left add_sentence ([],document.schedule, scheduler_state) new_sentences in
+  let sentences, schedule, _ = List.fold_left add_sentence ([],document.schedule, scheduler_state) parsed in
   sentences, schedule
 
 let create_document init_synterp_state text =

language-server/dm/documentManager.ml

@@ -317,22 +317,27 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve
         {state with execution_state}, events
 
 let reset_to_top st = { st with observe_id = Top }
+
 let coq_pilot_observe st position text =
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) position in
   match Document.find_sentence_before st.document loc with
   | None -> log @@ "COQ PILOT ON NON VALID POSITION"; [] (* HANDLE ERROR *)
   | Some {id} ->
     let sentences, sch = Document.parse_text_at_loc loc text st.document in
-    let vst_for_next_todo, todo = ExecutionManager.build_tasks_for (Document.schedule st.document) st.execution_state id in
-    let more_todo = ExecutionManager.build_tasks_for_sentences sch sentences in
-    let execute_task (execution_state, vst_for_next_todo) task = 
-      let (execution_state,vst_for_next_todo,_events,_interrupted) =
-      ExecutionManager.execute execution_state (vst_for_next_todo, [], false) task in
-      execution_state, vst_for_next_todo
+    let vst_for_next_todo, execution_state, task, _ = ExecutionManager.build_tasks_for st.document (Document.schedule st.document) st.execution_state id false in
+    let execution_state = ExecutionManager.build_tasks_for_sentences execution_state sch sentences in
+    let rec execute_task execution_state vst_for_next_todo task =
+      match task with
+      | None -> execution_state, vst_for_next_todo
+      | Some task ->
+        let (next, execution_state,vst_for_next_todo,_events,_interrupted) =
+        ExecutionManager.execute execution_state st.document (vst_for_next_todo, [], false) task false in
+        execute_task execution_state vst_for_next_todo next
     in
-    let execution_state, _ = List.fold_left execute_task (st.execution_state, vst_for_next_todo) (todo @ more_todo) in
+    let execution_state, _ = execute_task execution_state vst_for_next_todo task in
     let all_errors = ExecutionManager.all_errors execution_state in  (* TODO: RETURN ONLY THE NEW ERRORS *)
-    List.map (fun e -> Pp.string_of_ppcmds @@ snd (snd e)) all_errors
+    let get_pp_error (_, (_, pp, _)) = pp in
+    List.map (fun e -> Pp.string_of_ppcmds @@  get_pp_error e) all_errors
 
 let get_document_proofs st =
   let outline = Document.outline st.document in

language-server/dm/executionManager.ml

@@ -710,9 +710,10 @@ let build_tasks_for document sch st id block =
   | Some id, true ->
     vs, {st with todo=[]}, None, Some id
 
-let build_tasks_for_sentences sch sentences =
+let build_tasks_for_sentences st sch sentences =
   let tasks = List.map (fun ({id}: Document.sentence) -> snd @@ task_for_sentence sch id) sentences in
-  List.concat_map prepare_task tasks
+  let todo = List.concat_map prepare_task tasks in
+  {st with todo}
 
 let all_errors st =
   List.fold_left (fun acc (id, (p,_)) ->

language-server/dm/executionManager.mli

@@ -74,8 +74,8 @@ 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 * errored_sentence
-val build_tasks_for_sentences : Scheduler.schedule -> Document.sentence list -> prepared_task list
+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_sentences : state -> Scheduler.schedule -> Document.sentence list -> state
 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

language-server/vscoqtop/lspManager.ml

@@ -562,8 +562,8 @@ let sendCoqPilotResult id params =
   let Request.Client.CoqPilotParams.{ textDocument; position; text} = params in
   let uri = textDocument.uri in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[coqPilotResult] ignoring event on non existant document"; Error("Document does not exist"), []
-  | Some st -> 
+  | None -> log @@ "[coqPilotResult] ignoring event on non existant document"; Error({message="Document does not exist"; code=None}), []
+  | Some { st } -> 
     let errors = Dm.DocumentManager.coq_pilot_observe st position text in
     log "Sending errors for coqpilot request:";
     List.iter (fun e -> log e) errors;