Support diff mode

Closes #538

client/goal-view-ui/src/components/atoms/Goal.module.css

@@ -50,3 +50,21 @@
 .tactic-string {
   color: var(--vscode-coq-tacticString);
 }
+
+.diff-added {
+  background-color: var(--vscode-coq-addedCharacter);
+  text-decoration: underline;
+}
+
+.diff-added-bg {
+  background-color: var(--vscode-coq-addedCharacterBackground);
+}
+
+.diff-removed {
+  background-color: var(--vscode-coq-removedCharacter);
+  text-decoration: line-through;
+}
+
+.diff-removed-bg {
+  background-color: var(--vscode-coq-removedCharacterBackground);
+}

client/goal-view-ui/src/components/atoms/Hypothesis.module.css

@@ -21,7 +21,7 @@
     margin-left: 3pt;
 }
 
-.Type {
+.Content {
     color: var(--vscode-editor-foreground);
 }
 
@@ -68,4 +68,22 @@
 }
 .tactic-string {
   color: var(--vscode-coq-tacticString);
+}
+
+.diff-added {
+  background-color: var(--vscode-coq-addedCharacter);
+  text-decoration: underline;
+}
+
+.diff-added-bg {
+  background-color: var(--vscode-coq-addedCharacterBackground);
+}
+
+.diff-removed {
+  background-color: var(--vscode-coq-removedCharacter);
+  text-decoration: line-through;
+}
+
+.diff-removed-bg {
+  background-color: var(--vscode-coq-removedCharacterBackground);
 }

client/goal-view-ui/src/components/atoms/Hypothesis.tsx

@@ -5,28 +5,19 @@ import { PpString } from '../../types';
 import { fragmentOfPpString } from '../../utilities/pp';
 
 type HypothesisProps = {
-    identifiers: string[], 
-    type: PpString,
+    content: PpString,
 };
 
 const hypothesis: FunctionComponent<HypothesisProps> = (props) => {
 
-    const {identifiers, type} = props;
-
-    const idString = identifiers.slice(1).reduce((pre, curr) => {
-        return pre + ", " + curr;
-    }, identifiers[0]);
+    const {content} = props;
 
     return (
-        <li className={classes.Hypothesis}>
-            <span className={classes.IdentifierBlock}>
-                <span className={classes.Identifier}>{idString}</span>
-                <span className={classes.Separator}> : </span>
-            </span>
-            <span className={classes.Type}>{fragmentOfPpString(type, classes)}</span>
+        <div className={classes.Hypothesis}>
+            <span className={classes.Content}>{fragmentOfPpString(content, classes)}</span>
             <br/>
-        </li>
+        </div>
     );
 };
 
-export default hypothesis;
+export default hypothesis;

client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx

@@ -11,10 +11,7 @@ type CollapsibleGoalBlockProps = {
     goal: {
         id: string, 
         goal: PpString, 
-        hypotheses: {
-            identifiers: string[],
-            type: PpString, 
-        }[]
+        hypotheses: PpString[]
     },
     collapseHandler: (id: string) => void, 
     isOpen: boolean,

client/goal-view-ui/src/components/molecules/GoalBlock.tsx

@@ -13,10 +13,7 @@ type GoalBlockProps = {
     goal: {
         id: string, 
         goal: PpString, 
-        hypotheses: {
-            identifiers: string[],
-            type: PpString, 
-        }[]
+        hypotheses: PpString[]
     }
 };
 

client/goal-view-ui/src/components/molecules/HypothesesBlock.tsx

@@ -6,18 +6,15 @@ import classes from './HypothesesBlock.module.css';
 import { PpString } from '../../types';
 
 type HypothesesBlockProps = {
-    hypotheses: {
-        identifiers: string[], 
-        type: PpString,
-    }[];
+    hypotheses: PpString[];
 };
 
 const hypothesesBlock: FunctionComponent<HypothesesBlockProps> = (props) => {
 
     const {hypotheses} = props;
 
     const hypothesesComponents = hypotheses.map((hyp, index) => {
-        return <Hypothesis key={index} identifiers={hyp.identifiers} type={hyp.type} />;
+        return <Hypothesis key={index} content={hyp} />;
     });
 
     return (

client/goal-view-ui/src/components/organisms/GoalTabs.tsx

@@ -14,10 +14,7 @@ type GoalSectionProps = {
     goals: {
         id: string,
         goal: PpString, 
-        hypotheses: {
-            identifiers: string[],
-            type: PpString
-        }[]
+        hypotheses: PpString[]
     }[];
 };
 

client/goal-view-ui/src/types.ts

@@ -23,10 +23,7 @@ export type PpString =
 export type Goal = {
     id: string,
     goal: PpString, 
-    hypotheses: {
-        identifiers: string[],
-        type: PpString
-    }[],
+    hypotheses: PpString[],
     isOpen: boolean, 
     displayId: number
 };

client/goal-view-ui/src/utilities/pp.tsx

@@ -1,23 +1,48 @@
 import { ReactElement, ReactFragment } from 'react';
 import { PpString } from '../types';
 
-export const fragmentOfPpString = (pp:PpString, classes:CSSModuleClasses) : ReactFragment => {
+enum PpMode { vertical,  horizontal }
+
+const fragmentOfPpStringWithMode = (pp:PpString, mode: PpMode, classes:CSSModuleClasses) : ReactFragment => {
     switch (pp[0]) {
         case "Ppcmd_empty":
             return <></>;
         case "Ppcmd_string":
             return pp[1];
         case "Ppcmd_glue":
-            return pp[1].map(pp => fragmentOfPpString(pp, classes));
+            return pp[1].map(pp => fragmentOfPpStringWithMode(pp, mode, classes));
         case "Ppcmd_box":
-            return fragmentOfPpString(pp[2], classes);
+          switch (pp[1][0]) {
+              case "Pp_hbox":
+                  mode = PpMode.horizontal;
+                  break;
+              case "Pp_vbox":
+                  mode = PpMode.vertical;
+                  break;
+              case "Pp_hvbox":
+                  mode = PpMode.horizontal; // TODO proper support for hvbox
+                  break;
+              case "Pp_hovbox":
+                  mode = PpMode.horizontal; // TODO proper support for hovbox
+                  break;
+          };
+          return fragmentOfPpStringWithMode(pp[2], mode, classes);
         case "Ppcmd_tag":
-            return <span className={classes[pp[1].replace(".", "-")]}>{fragmentOfPpString(pp[2], classes)}</span>;
+            return <span className={classes[pp[1].replaceAll(".", "-")]}>{fragmentOfPpStringWithMode(pp[2], mode, classes)}</span>;
         case "Ppcmd_print_break":
-            return " ".repeat(pp[1]);
+            switch (mode) {
+                case PpMode.horizontal:
+                    return " ".repeat(pp[1]);
+                case PpMode.vertical:
+                    return <br/>;
+            }
         case "Ppcmd_force_newline":
             return <br/>;
         case "Ppcmd_comment":
             return pp[1];
     }
 };
+
+export const fragmentOfPpString = (pp:PpString, classes:CSSModuleClasses) : ReactFragment => {
+    return fragmentOfPpStringWithMode(pp, PpMode.horizontal, classes);
+};

client/package.json

@@ -118,6 +118,26 @@
             ],
             "default": "List",
             "description": "Determines wether multiple goals should be displayed in different tabs or as a list of collapsible items."
+          },
+          "vscoq.goals.diff.mode": {
+            "type": "string",
+            "enum": [
+              "off",
+              "on",
+              "removed"
+            ],
+            "default": "on",
+            "markdownDescription": "Enable/disable VsCoq's Proof View Diff. Only has acceptable performance on small goals."
+          },
+          "vscoq.goals.diff.addedTextIsItalic": {
+            "type": "boolean",
+            "default": false,
+            "markdownDescription": "If `true`, in the proof view, the diff will show added characters in italic. Note: the color of added characters can be changed in `#coq.addedCharacter#`."
+          },
+          "vscoq.goals.diff.removedTextIsStrikedthrough": {
+            "type": "boolean",
+            "default": false,
+            "markdownDescription": "If `true`, in the proof view, the diff will show removed characters with a line through. Note: the color of removed characters can be changed in `#coq.removedCharacter#`."
           }
         }
       },
@@ -498,16 +518,34 @@
         "id": "coq.addedCharacter",
         "description": "Color of added characters (in diffs).",
         "defaults": {
-          "dark": "#00fa001a",
+          "dark": "#00fa0033",
           "light": "#00fa0033",
           "highContrast": "#00fa0033"
         }
       },
+      {
+        "id": "coq.addedCharacterBackground",
+        "description": "Color of added characters (in diffs).",
+        "defaults": {
+          "dark": "#00fa000f",
+          "light": "#00fa000f",
+          "highContrast": "#00fa000f"
+        }
+      },
       {
         "id": "coq.removedCharacter",
         "description": "Color of removed characters (in diffs).",
         "defaults": {
-          "dark": "#fa000099",
+          "dark": "#fa000066",
+          "light": "#fa000066",
+          "highContrast": "#fa000066"
+        }
+      },
+      {
+        "id": "coq.removedCharacterBackground",
+        "description": "Color of removed characters (in diffs).",
+        "defaults": {
+          "dark": "#fa000033",
           "light": "#fa000033",
           "highContrast": "#fa000033"
         }

client/src/protocol/types.ts

@@ -44,15 +44,10 @@ interface Error {
     message: string; 
 }
 
-export interface Hypothesis {
-    identifiers: string[];
-    type: PpString;
-}
-
 export interface Goal {
     id: integer;
     goal: PpString;
-    hypotheses: Hypothesis[];
+    hypotheses: PpString[];
 }
 interface ProofViewNotificationType {
     goals: Goal[];
@@ -136,4 +131,4 @@ export interface DocumentStateRequest {
 
 export interface DocumentStateResponse {
     document: string;
-}
+}

client/testFixture/basic.v

@@ -1,3 +1,4 @@
-Definition foo := True.
-
-Definition bar := zar.
+Lemma foo : True -> True -> True.
+Proof.
+  intros H1. intros H2. intros H3.
+Qed.

language-server/dm/documentManager.ml

@@ -287,16 +287,21 @@ let handle_event ev st =
     let execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
     (Option.map (fun execution_state -> {st with execution_state}) execution_state_update, inject_em_events events)
 
-let get_proof st pos =
+let get_proof st diff_mode pos =
   let id_of_pos pos =
     let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
     match Document.find_sentence_before st.document loc with
     | None -> None
     | Some { id } -> Some id
   in
+  let previous_st id =
+    let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in
+    Option.bind oid (ExecutionManager.get_vernac_state st.execution_state)
+  in
   let oid = Option.cata id_of_pos st.observe_id pos in
   let ost = Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in
-  Option.bind ost ProofState.get_proof
+  let previous = Option.bind oid previous_st in
+  Option.bind ost (ProofState.get_proof ~previous diff_mode)
 
 let get_context st pos =
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in

language-server/dm/documentManager.mli

@@ -86,7 +86,7 @@ val feedbacks : state -> CoqFeedback.t list
 (** feedback [doc] returns notice, info and debug level feedbacks from coq corresponding
     to the sentences that have been executed in [doc]. *)
 
-val get_proof : state -> Position.t option -> ProofState.t option
+val get_proof : state -> Settings.Goals.Diff.Mode.t -> Position.t option -> ProofState.t option
 
 val get_completions : state -> Position.t -> (completion_item list, string) Result.t
 

language-server/protocol/printing.ml

@@ -11,6 +11,7 @@
 (*   See LICENSE file.                                                    *)
 (*                                                                        *)
 (**************************************************************************)
+open Util
 
 type pp_tag = string [@@deriving yojson]
 
@@ -32,10 +33,39 @@ type pp =
 | Ppcmd_comment of string list
 [@@deriving yojson]
 
+let rec regroup_tags_aux acc = function
+  | [] -> acc
+  | hd :: tl ->
+    match Pp.repr hd with
+    | Pp.Ppcmd_glue l ->
+      let acc = regroup_tags_aux acc l in
+      regroup_tags_aux acc tl
+    | Pp.Ppcmd_tag (s, pp) when String.starts_with ~prefix:Pp.start_pfx s ->
+      let pp = regroup_tags [pp] in
+      regroup_tags_aux (pp::acc) tl
+    | Pp.Ppcmd_tag (s, pp) when String.starts_with ~prefix:Pp.end_pfx s ->
+      let pp = regroup_tags [pp] in
+      let n = String.length Pp.end_pfx in
+      let tag = String.sub s n (String.length s - n) in
+      begin match acc with
+      | acc0::acc1::tlacc ->
+        let acc1 = Pp.tag tag (Pp.seq ((List.rev acc0) @ pp)) :: acc1 in
+        regroup_tags_aux (acc1 :: tlacc) tl
+      | _ -> failwith ("extra closing tag: " ^ tag)
+      end
+    | _ ->
+      let acc = (hd::List.hd acc)::List.tl acc in
+      regroup_tags_aux acc tl
+
+and regroup_tags l =
+ match regroup_tags_aux [[]] l with [l] -> List.rev l | _ -> failwith "tag not closed"
+
 let rec pp_of_coqpp t = match Pp.repr t with
   | Pp.Ppcmd_empty -> Ppcmd_empty
   | Pp.Ppcmd_string s -> Ppcmd_string s
-  | Pp.Ppcmd_glue l -> Ppcmd_glue (List.map pp_of_coqpp l)
+  | Pp.Ppcmd_glue l -> (* We are working around a Coq hack here *)
+    let l = regroup_tags l in
+    Ppcmd_glue (List.map pp_of_coqpp l)
   | Pp.Ppcmd_box (bt, pp) -> Ppcmd_box (bt, pp_of_coqpp pp)
   | Pp.Ppcmd_tag (tag, pp) -> Ppcmd_tag (tag, pp_of_coqpp pp)
   | Pp.Ppcmd_print_break (m,n) -> Ppcmd_print_break (m,n)