Add option to disable super-slow "Proof View Diff"

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,

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 {

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));
     }
@@ -1207,4 +1210,4 @@ function createDebuggingSentence(sent: State) : DSentence {
 //   public inspect() {
 //     return {cmd: this.cmd, range: this.range}
 //   }
-// }
+// }

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 */
@@ -191,16 +191,16 @@ 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);
     }
     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})});
   }
 
-}
+}