From 4a93ed2d3661901108999cfdac188ef6a5d78c07 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Tue, 13 Dec 2022 01:28:52 +0100 Subject: [PATCH 1/3] State.ts: Drop trailing whitespace --- server/src/stm/STM.ts | 2 +- server/src/stm/State.ts | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/server/src/stm/STM.ts b/server/src/stm/STM.ts index 7515247ee..d1c43fd1f 100644 --- a/server/src/stm/STM.ts +++ b/server/src/stm/STM.ts @@ -1207,4 +1207,4 @@ function createDebuggingSentence(sent: State) : DSentence { // public inspect() { // return {cmd: this.cmd, range: this.range} // } -// } \ No newline at end of file +// } diff --git a/server/src/stm/State.ts b/server/src/stm/State.ts index 2915a6bff..98c9e0a41 100644 --- a/server/src/stm/State.ts +++ b/server/src/stm/State.ts @@ -46,7 +46,7 @@ export class State { private diagnostics: CoqDiagnosticInternal[] = []; // set to true when a document change has invalidated the meaning of the associated sentence; this state needs to be cancelled private markedInvalidated = false; - private goal : ProofViewReference | null = null; + private goal : ProofViewReference | null = null; private constructor ( private commandText: string @@ -145,7 +145,7 @@ export class State { } public updateWorkerStatus(workerId: string, status: string) { - + } /** Handle sentence-status updates as they come from coqtop */ @@ -200,7 +200,7 @@ export class State { return diff.diffProofView(oldGoals, newGoals); } return newGoals; - } + } private translateDiagnostic(d : CoqDiagnosticInternal, delta: textUtil.RangeDelta) : void { if (d.range) { @@ -326,7 +326,7 @@ export class State { return textUtil.positionIsAfterOrEqual(this.textRange.start, position) || textUtil.positionIsAfter(this.textRange.end, position); } - + /** @returns `true` if this sentence contains `position`. */ public contains(position: Position) : boolean { return textUtil.positionIsBeforeOrEqual(this.textRange.start, position) && @@ -359,4 +359,4 @@ export class State { return this.diagnostics.map(function(d) { return Object.assign(d, {sentence: range})}); } -} \ No newline at end of file +} From d89806ea25bae74b545faf18635f6f77a16a327e Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Tue, 13 Dec 2022 01:27:16 +0100 Subject: [PATCH 2/3] Add `coq.proofDiff` option to disable proof diffs. Motivation: this option can be very slow, according to https://github.com/coq-community/vscoq/issues/317#issuecomment-1347425838. TODO: should probably be `coq.proofViewDiff`, but `coq.proofViewDiff.XYZ` options exist and I'll test for interference later. --- package.json | 5 +++++ server/src/protocol.ts | 1 + server/src/stm/STM.ts | 7 +++++-- server/src/stm/State.ts | 4 ++-- 4 files changed, 13 insertions(+), 4 deletions(-) diff --git a/package.json b/package.json index 5305dde02..35f9c3aa9 100644 --- a/package.json +++ b/package.json @@ -129,6 +129,11 @@ "default": "first-interaction", "description": "Create the proof view when a Coq script is opened, the user first interacts with coqtop, or else let the user do it manually." }, + "coq.proofViewDiff": { + "type": "boolean", + "default": "true", + "markdownDescription": "Enable/disable VsCoq's Proof View Diff. Only has acceptable performance on small goals." + }, "coq.proofViewDiff.addedTextIsItalic": { "type": "boolean", "default": false, diff --git a/server/src/protocol.ts b/server/src/protocol.ts index 72df74f35..e16cd56d7 100644 --- a/server/src/protocol.ts +++ b/server/src/protocol.ts @@ -77,6 +77,7 @@ export interface CoqSettings { /** After each command, check sentence-states for inconsistencies */ checkSentenceStateConsistency?: boolean, } + proofViewDiff: boolean } export interface FailValue { diff --git a/server/src/stm/STM.ts b/server/src/stm/STM.ts index d1c43fd1f..9e8685182 100644 --- a/server/src/stm/STM.ts +++ b/server/src/stm/STM.ts @@ -420,6 +420,9 @@ export class CoqStateMachine { endCommand(); } } + private get proofViewDiff(): boolean { + return server.project.settings.coq.proofViewDiff + } /** * Return the cached goal for the given position @@ -429,7 +432,7 @@ export class CoqStateMachine { try { const state = (direction==="subsequent" ? this.getStateAt(pos) : null) || this.getPrecedingStateAt(pos); if(state && state.hasGoal()) - return Object.assign({type: 'proof-view'} as {type: 'proof-view'}, state.getGoal(this.goalsCache)); + return Object.assign({type: 'proof-view'} as {type: 'proof-view'}, state.getGoal(this.goalsCache, this.proofViewDiff)); else return {type: "no-proof"} } catch(error) { @@ -857,7 +860,7 @@ private routeId = 1; focus: this.getFocusedPosition() }); this.focusedSentence.setGoal(pv); - return {type: 'proof-view', ...this.focusedSentence.getGoal(this.goalsCache)}; + return {type: 'proof-view', ...this.focusedSentence.getGoal(this.goalsCache, this.proofViewDiff)}; default: this.console.warn("Goal returned an unexpected value: " + util.inspect(goals,false,undefined)); } diff --git a/server/src/stm/State.ts b/server/src/stm/State.ts index 98c9e0a41..724defb5f 100644 --- a/server/src/stm/State.ts +++ b/server/src/stm/State.ts @@ -191,11 +191,11 @@ export class State { this.goal = goal; } - public getGoal(goalsCache: GoalsCache) : ProofView|null { + public getGoal(goalsCache: GoalsCache, proofViewDiff : boolean) : ProofView|null { if(!this.goal) return null; const newGoals = {...goalsCache.getProofView(this.goal), focus: this.textRange.end}; - if(this.prev && this.prev.goal) { + if(this.prev && this.prev.goal && proofViewDiff) { const oldGoals = goalsCache.getProofView(this.prev.goal); return diff.diffProofView(oldGoals, newGoals); } From 360b86e0867e58bb8e0b5ffa23dece864f254177 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Tue, 13 Dec 2022 02:27:50 +0100 Subject: [PATCH 3/3] STM.proofViewDiff: from server.project to this.project --- server/src/stm/STM.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/src/stm/STM.ts b/server/src/stm/STM.ts index 9e8685182..4961b63fb 100644 --- a/server/src/stm/STM.ts +++ b/server/src/stm/STM.ts @@ -421,7 +421,7 @@ export class CoqStateMachine { } } private get proofViewDiff(): boolean { - return server.project.settings.coq.proofViewDiff + return this.project.settings.coq.proofViewDiff } /**