Add coq.proofDiff option to disable proof diffs.

Motivation: this option can be very slow, according to
#317 (comment).

TODO: should probably be `coq.proofViewDiff`, but `coq.proofViewDiff.XYZ`
options exist and I'll test for interference later.

Author: Blaisorblade

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));
     }

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);
     }