converter.ts - handle done tactic properly

Paper-Proof · Nov 8, 2023 · 47dd21d · 47dd21d
1 parent 2a0ee37
commit 47dd21d
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 13 deletions.
diff --git a/...c/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts b/...c/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts
@@ -181,12 +181,12 @@ const createWindowInsides = (shared: UIShared, parentId: TLParentId | undefined,
     );
     let tacticEl : UIElement;
     if (tactic) {
-      const isSuccessTactic = tactic.successGoalId && tactic.text !== "sorry";
+      const isSuccessTactic = tactic.successGoalId && tactic.text !== "sorry" && tactic.text !== "done";
       tacticEl = createNode(shared, parentId, (isSuccessTactic ? `🎉 ${tactic.text} 🎉` : tactic.text), "tactic", CreateId.goalTactic(tactic.id));
     } else {
       tacticEl = createNode(shared, parentId, "...", "tactic", createShapeId());
     }
-    const isLastGoalNode = (tactic && tactic.successGoalId && tactic.text !== "sorry") || !tactic;
+    const isLastGoalNode = (tactic && tactic.successGoalId) || !tactic;
     if (isLastGoalNode) {
       goalAndTacticEls.push(withWidth(() => windowWidth, tacticEl), goalEl);
     } else {

diff --git a/app/src/services/updateUI/services/converter.ts b/app/src/services/updateUI/services/converter.ts
@@ -246,17 +246,31 @@ const handleTacticApp = (
   if (relevantGoalsAfter.length === 0) {
     const nextGoal = tactic.goalsAfter[0];
 
-    pretty.tactics.push({
-      id: newTacticId(),
-      text: tactic.tacticString,
-      dependsOnIds: tactic.tacticDependsOn,
-      goalArrows: [],
-      hypArrows: [],
-      // success arrows are better not drawn (noisy!), we should just mark the tactic as 🎉.
-      // .dependsOnIds will convey all the information we want to see.
-      successGoalId: mainGoalBefore.id,
-      haveWindowIds,
-    });
+    // `done` has a very unusual behaviour -
+    // if we had some goals prior to it, then it's a "fake success" tactic for all of them
+    if (tactic.tacticString === "done") {
+      tactic.goalsBefore.forEach((goalBefore) => {
+        pretty.tactics.push({
+          id: newTacticId(),
+          text: "done",
+          dependsOnIds: [],
+          goalArrows: [],
+          hypArrows: [],
+          successGoalId: goalBefore.id,
+          haveWindowIds,
+        });
+      })
+    } else {
+      pretty.tactics.push({
+        id: newTacticId(),
+        text: tactic.tacticString,
+        dependsOnIds: tactic.tacticDependsOn,
+        goalArrows: [],
+        hypArrows: [],
+        successGoalId: mainGoalBefore.id,
+        haveWindowIds,
+      });
+    }
   }
   // - we updated the goal!
   else if (relevantGoalsAfter.length === 1) {
@@ -468,6 +482,8 @@ const converter = (leanProofTree: LeanProofTree) : ConvertedProofTree => {
   // Then, draw all the other tactics and hypotheses and goals.
   recursive(leanProofTree, pretty);
 
+  console.log({ leanProofTree, convertedProofTree: postprocess(pretty) });
+
   return postprocess(pretty);
 }