From 08753492fff0137f195e946c500a271f95d24e96 Mon Sep 17 00:00:00 2001 From: Abdelghani Alidra Date: Thu, 18 Apr 2024 18:56:44 +0200 Subject: [PATCH 1/7] fix parsing error : return commands even when the end of the file contains parsing error --- src/lsp/lp_doc.ml | 42 ++++++++++++++++++------------------------ src/pure/pure.ml | 34 ++++++++++++++-------------------- src/pure/pure.mli | 14 ++++++-------- 3 files changed, 38 insertions(+), 52 deletions(-) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 48d437f6e..431d608f2 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) -> ((1, msg), Some pos)::logs, (pos,1,msg,None)::diags + 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/pure/pure.ml b/src/pure/pure.ml index db8b33e9e..192f6e7cd 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -58,29 +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 - 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. *) From 8265f126d7d0486f09bddd1000f9b1d016999ea9 Mon Sep 17 00:00:00 2001 From: Abdelghani Alidra Date: Fri, 19 Apr 2024 09:28:07 +0200 Subject: [PATCH 2/7] fix parsing error : add parsing error at the end of logs instead of the begining --- src/lsp/lp_doc.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 431d608f2..4bd40cce8 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -185,7 +185,7 @@ let check_text ~doc = let logs, diags = match error with | None -> logs, diags - | Some(pos,msg) -> ((1, msg), Some pos)::logs, (pos,1,msg,None)::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 From 0af043f0da098fde7a2448d242485d7865bc75ef Mon Sep 17 00:00:00 2001 From: Abdelghani Alidra Date: Wed, 24 Apr 2024 16:30:41 +0200 Subject: [PATCH 3/7] move green curson to the end of the current command instead of the begin of the line to display logs related to missing tokens at the end of the file --- editors/vscode/src/client.ts | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index 7ee27277e..ac56fa2fe 100644 --- a/editors/vscode/src/client.ts +++ b/editors/vscode/src/client.ts @@ -183,8 +183,10 @@ function checkProofUntilCursor(context: ExtensionContext) { //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); + // if (cursorPosition.character != 0) + // cursorPosition = new Position(cursorPosition.line, 0); + + cursorPosition = stepCommand(openEditor.document, cursorPosition, true); context.workspaceState.update('proofState', cursorPosition); //proof state is set to the cursor position From 146cb48b60b3fadad647bcee0558f10b629c7968 Mon Sep 17 00:00:00 2001 From: Abdelghani Alidra Date: Wed, 24 Apr 2024 15:49:20 +0200 Subject: [PATCH 4/7] fix position of green cursor when navigating proofs in the presence of opening braket --- editors/vscode/src/client.ts | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index ac56fa2fe..082ad0c95 100644 --- a/editors/vscode/src/client.ts +++ b/editors/vscode/src/client.ts @@ -511,7 +511,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)); From bdd33fb6c2dc40eefed399cb177d7d41be4bfe77 Mon Sep 17 00:00:00 2001 From: Abdelghani Alidra Date: Wed, 24 Apr 2024 19:47:52 +0200 Subject: [PATCH 5/7] fix green cursor position when using ctrl + enter navigation --- editors/vscode/src/client.ts | 7 ------- 1 file changed, 7 deletions(-) diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index 082ad0c95..a1b6f2d57 100644 --- a/editors/vscode/src/client.ts +++ b/editors/vscode/src/client.ts @@ -178,13 +178,6 @@ 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); cursorPosition = stepCommand(openEditor.document, cursorPosition, true); From cca8f91b4e9eb80c4f0eedd7b13c495d4feceab6 Mon Sep 17 00:00:00 2001 From: Abdelghani Alidra Date: Wed, 24 Apr 2024 19:58:52 +0200 Subject: [PATCH 6/7] Only consider logs that are attached to commands whome starting positions are beyound the cursor --- src/lsp/lp_lsp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 0dca0b7dc65b401ebf7589e6bd54fd433296250d Mon Sep 17 00:00:00 2001 From: Abdelghani Alidra Date: Fri, 26 Apr 2024 12:10:23 +0200 Subject: [PATCH 7/7] fix position of green cursor with check until cursor command to be more accurate --- editors/vscode/src/client.ts | 38 +++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index a1b6f2d57..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) @@ -179,7 +207,15 @@ function checkProofUntilCursor(context: ExtensionContext) { //The current position of the cursor let cursorPosition: Position = openEditor.selection.active; - cursorPosition = stepCommand(openEditor.document, cursorPosition, true); + 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