From 47dd21da64d8b1ce42a5f1fe921e96072e376023 Mon Sep 17 00:00:00 2001 From: Evgenia Karunus Date: Wed, 8 Nov 2023 20:22:38 +0400 Subject: [PATCH] converter.ts - handle `done` tactic properly --- .../CreateElement/createWindowInsides.ts | 4 +- .../services/updateUI/services/converter.ts | 38 +++++++++++++------ 2 files changed, 29 insertions(+), 13 deletions(-) diff --git a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts b/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts index 17aa741..66f1038 100644 --- a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts +++ b/app/src/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 index 7d7a76a..d257dd7 100644 --- 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); }