fix parsing error : return commands even when the end of the file contains parsing error

editors/vscode/src/client.ts

@@ -163,6 +163,34 @@ function checkProofBackward(context: ExtensionContext) {
 
 function checkProofUntilCursor(context: ExtensionContext) {
 
+    function previousCaracterSkippingSpaces(document: TextDocument, currentPos: Position) {
+        const index = document.offsetAt(currentPos)
+        const slicedText = document.getText().slice(0, index);
+
+    // Match the last letter before a series of spaces and tabulations
+        const regex =/(\S)(?=[ \t]*$)/;
+
+    // Find the last letter before spaces
+        let myMatch = slicedText.match(regex);
+
+    // return the last letter if found
+        return myMatch ? myMatch[1] : null;
+    }
+
+    function nextCaracterSkippingSpaces(document: TextDocument, currentPos: Position) {
+        const index = document.offsetAt(currentPos)
+        const slicedText = document.getText().slice(index);
+
+    // Match the last letter after spaces and tabulations
+        const regex = /(\S)(?=[ \t]*$)/;
+
+    // Find the last letter after spaces
+        let myMatch = slicedText.split(/\r?\n/)[0].match(regex);
+
+    // return the last letter if found
+        return myMatch ? myMatch[0] : null;
+    }
+
     //Checking workspace
     const openEditor: TextEditor | undefined = window.activeTextEditor;
     if (!openEditor)
@@ -178,13 +206,16 @@ function checkProofUntilCursor(context: ExtensionContext) {
 
     //The current position of the cursor
     let cursorPosition: Position = openEditor.selection.active;
-    if (proofState.line == cursorPosition.line)
-        return;
 
-    //To simplify the code, proof states are always at the beggining of the highlighted line
-    //So must be the cursor position since it is the new proof state
-    if (cursorPosition.character != 0)
-        cursorPosition = new Position(cursorPosition.line, 0);
+    const cursorIsAtEndOfCommand = previousCaracterSkippingSpaces(openEditor.document, cursorPosition) === ";";
+    const commandExistsAfterCursorinSameLine = nextCaracterSkippingSpaces(openEditor.document, cursorPosition) != null;
+
+    // If the cursor is at the begining or in the middle of a command or there are more commands in the same line,
+    // then do not move the green zone further.
+    // Else, stop at the current position
+    if(!cursorIsAtEndOfCommand || commandExistsAfterCursorinSameLine) {
+        cursorPosition = stepCommand(openEditor.document, cursorPosition, true);
+    }
 
     context.workspaceState.update('proofState', cursorPosition); //proof state is set to the cursor position
 
@@ -509,7 +540,11 @@ function stepCommand(document: TextDocument, currentPos: Position, forward: bool
     const termRegex = new RegExp(terminators.join("|"), 'gi');
 
     let termPositions = [...document.getText().matchAll(termRegex)]
-        .map(rm => rm.index ? rm.index + rm[0].length : undefined)
+        .map(rm => { 
+            if (rm[0] === ";") {
+                return rm.index ? rm.index + rm[0].length : undefined
+            }
+            else return rm.index ? rm.index : undefined })
         .filter((x): x is number => x !== undefined) // remove undefined
         .map(x => document.positionAt(x));
 

src/lsp/lp_doc.ml

@@ -164,35 +164,29 @@ let dummy_loc =
 
 let check_text ~doc =
   let uri, version = doc.uri, doc.version in
+  let cmds, error = Pure.parse_text ~fname:uri doc.text in
   let root =
     match doc.root with
-    | Some(ss) -> ss
+    | Some ss -> ss
     | None ->
-      raise(Error.fatal_no_pos "Root state is missing
-      probably because new_doc has raised exception")
+        raise(Error.fatal_no_pos "Root state is missing probably because \
+                                  new_doc raised an exception")
   in
-  try
-    let cmds =
-      let (cmds, root) = Pure.parse_text root ~fname:uri doc.text in
-      (* One shot state update after parsing. *)
-      doc.root <- Some(root); doc.final <- Some(root); cmds
-    in
-
-    (* compute rangemap *)
-    let map = Pure.rangemap cmds in
-
-    let nodes, final, diag, logs =
-      List.fold_left (process_cmd uri) ([],root,[],[]) cmds in
-    let logs = List.rev logs in
-    let doc = { doc with nodes; final=Some(final); map; logs } in
-    doc,
-    LSP.mk_diagnostics ~uri ~version @@
+  let nodes, final, diags, logs =
+    List.fold_left (process_cmd uri) ([],root,[],[]) cmds in
+  let logs = List.rev logs
+  and diags = (* filter out diagnostics with no position *)
     List.fold_left (fun acc (pos,lvl,msg,goal) ->
         match pos with
         | None     -> acc
         | Some pos -> (pos,lvl,msg,goal) :: acc
-      ) [] diag
-  with
-  | Pure.Parse_error(loc, msg) ->
-    let logs = [((1, msg), Some loc)] in
-    {doc with logs}, mk_error ~doc loc msg
+      ) [] diags
+  in
+  let logs, diags =
+    match error with
+    | None -> logs, diags
+    | Some(pos,msg) -> logs @ [((1, msg), Some pos)], diags @ [pos,1,msg,None]
+  in
+  let map = Pure.rangemap cmds in
+  let doc = { doc with nodes; final=Some(final); map; logs } in
+  doc, LSP.mk_diagnostics ~uri ~version diags

src/lsp/lp_lsp.ml

@@ -294,7 +294,7 @@ let get_logs ~doc ~line ~pos : string =
       (fun ((_,msg),loc) ->
          match loc with
          | Some Pos.{start_line; start_col; _}
-           when compare (start_line,start_col) end_limit <= 0 -> Some msg
+           when compare (start_line,start_col) end_limit < 0 -> Some msg
          | _ -> None)
       doc.Lp_doc.logs
   in

src/pure/pure.ml

@@ -58,30 +58,23 @@ end
 type state = Time.t * Sig_state.t
 
 (** Exception raised by [parse_text] on error. *)
-exception Parse_error of Pos.pos * string
 
-let parse_text : state -> fname:string -> string -> Command.t list * state =
-    fun (t,st) ~fname s ->
-  let dk_syntax = Filename.check_suffix fname dk_src_extension in
+let parse_text :
+      fname:string -> string -> Command.t list * (Pos.pos * string) option =
+  fun ~fname s ->
+  let parse_string =
+    if Filename.check_suffix fname dk_src_extension then
+      Parser.Dk.parse_string
+    else Parser.parse_string
+  in
+  let cmds = Stdlib.ref [] in
   try
-    LibMeta.reset_meta_counter();
-    Time.restore t;
-    let ast =
-      let strm =
-        if dk_syntax then Parser.Dk.parse_string fname s
-        else Parser.parse_string fname s
-      in
-      (* NOTE this processing could be avoided with a parser for a list of
-         commands. Such a parser is not trivially done. *)
-      let cmds = Stdlib.ref [] in
-      Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) strm;
-      List.rev Stdlib.(!cmds)
-    in
-    (ast, (Time.save (), st))
+    Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) (parse_string fname s);
+    List.rev Stdlib.(!cmds), None
   with
-  | Fatal(Some(Some(pos)), msg) -> raise (Parse_error(pos, msg))
-  | Fatal(Some(None)     , _  ) -> assert false (* Should not produce. *)
-  | Fatal(None           , _  ) -> assert false (* Should not produce. *)
+  | Fatal(Some(Some(pos)), msg) -> List.rev Stdlib.(!cmds), Some(pos, msg)
+  | Fatal(Some(None)     , _  ) -> assert false
+  | Fatal(None           , _  ) -> assert false
 
 type proof_finalizer = Sig_state.t -> Proof.proof_state -> Sig_state.t
 

src/pure/pure.mli

@@ -35,14 +35,12 @@ type state
 (** Representation of the state when in a proof. *)
 type proof_state
 
-(** Exception raised by [parse_text]. *)
-exception Parse_error of Pos.pos * string
-
-(** [parse_text st ~fname contents] runs the parser on the string [contents]
-   as if it were a file named [fname]. The action takes place in the state
-   [st], and an updated state is returned. The function may raise
-   [Parse_error]. *)
-val parse_text : state -> fname:string -> string -> Command.t list * state
+(** [parse_text ~fname contents] runs the parser on the string [contents] as
+    if it were a file named [fname]. It returns the list of commands it could
+    parse and, either [None] if it could parse all commands, or some position
+    and error message otherwise. *)
+    val parse_text :
+    fname:string -> string -> Command.t list * (Pos.pos * string) option
 
 (** A goal is given by a list of assumptions and a conclusion. Each assumption
    has a name and a type. *)