diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index 7ee27277e..990f0cf2c 100644 --- a/editors/vscode/src/client.ts +++ b/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)); diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 48d437f6e..4bd40cce8 100644 --- a/src/lsp/lp_doc.ml +++ b/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 diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 7023d40f2..eecd1ab2c 100644 --- a/src/lsp/lp_lsp.ml +++ b/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 diff --git a/src/pure/pure.ml b/src/pure/pure.ml index cb7ce7a2f..192f6e7cd 100644 --- a/src/pure/pure.ml +++ b/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 diff --git a/src/pure/pure.mli b/src/pure/pure.mli index a9b532c8d..0ac8f2e08 100644 --- a/src/pure/pure.mli +++ b/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. *)