Cancel parsing event

client/src/extension.ts

@@ -41,8 +41,8 @@
     sendStepBackward
 } from './manualChecking';
 import { 
     makeVersionedDocumentId,
     isMouseOrKeyboardEvent
 } from './utilities/utils';
 import { DocumentStateViewProvider } from './panels/DocumentStateViewProvider';
 import VsCoqToolchainManager, {ToolchainError, ToolChainErrorCode} from './utilities/toolchain';
@@ -193,7 +193,7 @@
             const req = new RequestType<ResetCoqRequest, ResetCoqResponse, void>("vscoq/resetCoq");
             Client.writeToVscoq2Channel(uri.toString());
             client.sendRequest(req, params).then(
                 (res) => {
                     GoalPanel.resetGoalPanel();
                 }, 
                 (err) => {
@@ -211,28 +211,8 @@
         registerVscoqTextCommand('expandAllQueries', () => searchProvider.expandAll());
         registerVscoqTextCommand('interpretToPoint', (editor) => sendInterpretToPoint(editor, client));
         registerVscoqTextCommand('interpretToEnd', (editor) => sendInterpretToEnd(editor, client));
-        registerVscoqTextCommand('stepForward', (editor) => {
-
-            if(workspace.getConfiguration('vscoq.proof').mode === 1) {
-                const textDocument = makeVersionedDocumentId(editor);
-                const position = editor.selection.active;
-                client.sendNotification("vscoq/stepForward", {textDocument: textDocument, position: position});
-            }
-            else {
-                sendStepForward(editor, client);
-            }
-
-        });
-        registerVscoqTextCommand('stepBackward', (editor) => {
-            if(workspace.getConfiguration('vscoq.proof').mode === 1) {
-                const textDocument = makeVersionedDocumentId(editor);
-                const position = editor.selection.active;
-                client.sendNotification("vscoq/stepBackward", {textDocument: textDocument, position: position});
-            }
-            else {
-                sendStepBackward(editor, client);
-            }
-        });
+        registerVscoqTextCommand('stepForward', (editor) => sendStepForward(editor, client));
+        registerVscoqTextCommand('stepBackward', (editor) => sendStepBackward(editor, client));
         registerVscoqTextCommand('documentState', async (editor) => {
 
             documentStateProvider.setDocumentUri(editor.document.uri);
@@ -371,7 +351,7 @@
                 }
             }));
 
             let goalsHook = window.onDidChangeTextEditorSelection(
                 (evt: TextEditorSelectionChangeEvent) => {                    
                     if (evt.textEditor.document.languageId === "coq"
                         && workspace.getConfiguration('vscoq.proof').mode === 1)
@@ -381,7 +361,7 @@
                 }
             );
 
             window.onDidChangeActiveTextEditor(editor => {
                 client.updateHightlights();
             });
 

client/src/manualChecking.ts

@@ -1,6 +1,6 @@
 import {
     TextEditor,
     commands,
     workspace
 } from 'vscode';
 
@@ -27,11 +27,11 @@
 
 export const sendStepForward = (editor: TextEditor,  client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
-    client.sendNotification("vscoq/stepForward", {textDocument: textDocument, position: null});
+    client.sendNotification("vscoq/stepForward", {textDocument: textDocument});
 };
 
 export const sendStepBackward = (editor: TextEditor,  client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
-    client.sendNotification("vscoq/stepBackward", {textDocument: textDocument, position: null});
+    client.sendNotification("vscoq/stepBackward", {textDocument: textDocument});
 };
 

language-server/dm/document.ml

@@ -90,8 +90,43 @@ type document = {
   parsed_loc : int;
   raw_doc : RawDocument.t;
   init_synterp_state : Vernacstate.Synterp.t;
+  cancel_handle: Sel.Event.cancellation_handle option;
 }
 
+type parse_state = {
+  started: float;
+  stop: int;
+  top_id: sentence_id option;
+  loc: Loc.t option;
+  synterp_state : Vernacstate.Synterp.t;
+  stream: (unit, char) Gramlib.Stream.t;
+  raw: RawDocument.t;
+  parsed: pre_sentence list;
+  errors: parsing_error list;
+  parsed_comments: comment list;
+  previous_document: document;
+}
+
+type parsing_end_info = {
+    unchanged_id: sentence_id option;
+    invalid_ids: sentence_id_set;
+    previous_document: document;
+    parsed_document: document;
+}
+
+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
+
+let create_parsing_event event =
+  let priority = Some PriorityManager.parsing in
+  Sel.now ?priority event
+
 let range_of_sentence raw (sentence : sentence) =
   let start = RawDocument.position_of_loc raw sentence.start in
   let end_ = RawDocument.position_of_loc raw sentence.stop in
@@ -440,21 +475,22 @@ let get_entry ast =
 [%%endif]
 
 
-let rec parse_more ?loc synterp_state stream raw parsed parsed_comments errors =
-  let handle_parse_error start msg qf =
-    log @@ "handling parse error at " ^ string_of_int start;
-    let stop = Stream.count stream in
-    let parsing_error = { msg; start; stop; qf} in
-    let errors = parsing_error :: errors in
-    (* TODO: we could count the \n between start and stop and increase Loc.line_nb *)
-    parse_more ?loc synterp_state stream raw parsed parsed_comments errors
-  in
+let handle_parse_error start msg qf ({stream; errors;} as parse_state) =
+  log @@ "handling parse error at " ^ string_of_int start;
+  let stop = Stream.count stream in
+  let parsing_error = { msg; start; stop; qf} in
+  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)
+
+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 *) -> List.rev parsed, errors, List.rev parsed_comments
+    | None, _ (* EOI *) -> create_parsing_event (Invalidate parse_state)
     | Some ast, comments ->
       let stop = Stream.count stream in
       log @@ "Parsed: " ^ (Pp.string_of_ppcmds @@ Ppvernac.pr_vernac ast);
@@ -476,34 +512,33 @@ let rec parse_more ?loc synterp_state stream raw parsed parsed_comments errors =
           let parsed = sentence :: parsed in
           let comments = List.map (fun ((start, stop), content) -> {start; stop; content}) comments in
           let parsed_comments = List.append comments parsed_comments in
-          parse_more ?loc:ast.loc synterp_state stream raw parsed parsed_comments errors
+          let loc = ast.loc in
+          let parse_state = {parse_state with parsed_comments; parsed; loc; synterp_state} in
+          create_parsing_event (ParseEvent parse_state)
         with exn ->
           let e, info = Exninfo.capture exn in
           let loc = get_loc_from_info_or_exn e info in
           let qf = Result.value ~default:[] @@ Quickfix.from_exception e in
-          handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf)
+          handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) parse_state
         end
     | exception (E msg as exn) ->
       let loc = Loc.get_loc @@ Exninfo.info exn in
       let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
       junk_sentence_end stream;
-      handle_parse_error start (loc,msg) (Some qf)
+      handle_parse_error start (loc,msg) (Some qf) {parse_state with stream}
     | exception (CLexer.Error.E e as exn) -> (* May be more problematic to handle for the diff *)
       let loc = Loc.get_loc @@ Exninfo.info exn in
       let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
       junk_sentence_end stream;
-      handle_parse_error start (loc,CLexer.Error.to_string e) (Some qf)
+      handle_parse_error start (loc,CLexer.Error.to_string e) (Some qf) {parse_state with stream}
     | exception exn ->
       let e, info = Exninfo.capture exn in
       let loc = Loc.get_loc @@ info in
       let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
       junk_sentence_end stream;
-      handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf)
+      handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) {parse_state with stream}
   end
 
-let parse_more synterp_state stream raw =
-  parse_more synterp_state stream raw [] [] []
-
 let rec unchanged_id id = function
   | [] -> id
   | Equal s :: diffs ->
@@ -548,7 +583,9 @@ let invalidate top_edit top_id parsed_doc new_sentences =
   unchanged_id, invalid_ids, doc
 
 (** Validate document when raw text has changed *)
-let validate_document ({ parsed_loc; raw_doc; } as document) =
+let validate_document ({ parsed_loc; raw_doc; cancel_handle } as document) =
+  (* Cancel any previous parsing event *)
+  Option.iter Sel.Event.cancel cancel_handle;
   (* We take the state strictly before parsed_loc to cover the case when the
   end of the sentence is editted *)
   let (stop, synterp_state, _scheduler_state) = state_strictly_before document parsed_loc in
@@ -558,11 +595,25 @@ let validate_document ({ parsed_loc; raw_doc; } as document) =
   let stream = Stream.of_string text in
   while Stream.count stream < stop do Stream.junk () stream done;
   log @@ Format.sprintf "Parsing more from pos %i" stop;
-  let errors = parsing_errors_before document stop in
-  let comments = comments_before document stop in
-  let new_sentences, new_errors, new_comments = parse_more synterp_state stream raw_doc (* TODO invalidate first *) in
+  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 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
+  {document with cancel_handle}, [Sel.now ?priority (ParseEvent parsed_state)]
+
+let handle_invalidate {parsed; errors; parsed_comments; stop; top_id; started; previous_document} document =
+  let end_ = Unix.gettimeofday ()in
+  let time = end_ -. started in
+  (* log @@ Format.sprintf "Parsing phase ended in %5.3f" time; *)
+  log @@ Format.sprintf "Parsing phase ended in %5.3f\n%!" time;
+  let new_sentences = List.rev parsed in
+  let new_comments = List.rev parsed_comments in
+  let new_errors = errors in
   log @@ Format.sprintf "%i new sentences" (List.length new_sentences);
   log @@ Format.sprintf "%i new comments" (List.length new_comments);
+  let errors = parsing_errors_before document stop in
+  let comments = comments_before document stop in
   let unchanged_id, invalid_ids, document = invalidate (stop+1) top_id document new_sentences in
   let parsing_errors_by_end =
     List.fold_left (fun acc (error : parsing_error) -> LM.add error.stop error acc) errors new_errors
@@ -571,11 +622,20 @@ let validate_document ({ parsed_loc; raw_doc; } as document) =
     List.fold_left (fun acc (comment : comment) -> LM.add comment.stop comment acc) comments new_comments
   in
   let parsed_loc = pos_at_end document in
-  unchanged_id, invalid_ids, { document with parsed_loc; parsing_errors_by_end; comments_by_end}
+  let parsed_document = {document with parsed_loc; parsing_errors_by_end; comments_by_end} in
+  Some {parsed_document; unchanged_id; invalid_ids; previous_document}
+
+let handle_event document = function
+| ParseEvent state -> 
+  let event = handle_parse_more state 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 create_document init_synterp_state text =
   let raw_doc = RawDocument.create text in
-    { parsed_loc = -1;
+    { 
+      parsed_loc = -1;
       raw_doc;
       sentences_by_id = SM.empty;
       sentences_by_end = LM.empty;
@@ -584,6 +644,7 @@ let create_document init_synterp_state text =
       schedule = initial_schedule;
       outline = [];
       init_synterp_state;
+      cancel_handle = None;
     }
 
 let apply_text_edit document edit =

language-server/dm/document.mli

@@ -37,6 +37,19 @@ type outline_element = {
 
 type outline = outline_element list
 
+
+type parsing_end_info = {
+    unchanged_id: sentence_id option;
+    invalid_ids: sentence_id_set;
+    previous_document: document;
+    parsed_document: document;
+}
+
+type event
+val pp_event : Format.formatter -> event -> unit
+
+type events = event Sel.Event.t list
+
 val raw_document : document -> RawDocument.t
 
 val outline : document -> outline
@@ -45,10 +58,15 @@ val create_document : Vernacstate.Synterp.t -> string -> document
 (** [create_document init_synterp_state text] creates a fresh document with content defined by
     [text] under [init_synterp_state]. *)
 
-val validate_document : document -> sentence_id option * sentence_id_set * document
-(** [validate_document doc] parses the document without forcing any execution
-    and returns the id of the bottommost sentence of the prefix which has not changed
-    since the previous validation, as well as the set of invalidated sentences *)
+val validate_document : document -> document * events
+(** [validate_document doc] triggers the parsing of the document line by line without
+    launching any execution. *)
+
+val handle_event : document -> event -> document * events * parsing_end_info option
+(** [handle_event dpc ev] handles a parsing event for the document. One parsing event parses one line
+    and prepares the next parsing event. Finally once the full parsing is done, the final event returs
+    the id of the bottomost sentence of the prefix which has not changed since the previous validation
+    as well as the set of invalidated sentences. *)
 
 type parsed_ast = {
   ast: Synterp.vernac_control_entry;
@@ -63,6 +81,8 @@ type parsing_error = {
   qf: Quickfix.t list option;
 }
 
+type parse_state
+
 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 *)