No longer adds to proof structure if illegal move

RAIRLab · Nov 26, 2023 · 541b4a8 · 541b4a8
1 parent 0e95eb6
commit 541b4a8
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 43 deletions.
diff --git a/src/ProofTools/ProofMoveMultiTool.ts b/src/ProofTools/ProofMoveMultiTool.ts
@@ -11,7 +11,7 @@ import {AtomNode} from "../AEG/AtomNode";
 import {CutNode} from "../AEG/CutNode";
 import {treeContext} from "../treeContext";
 import {offset} from "../DrawModes/DragTool";
-import {drawAtom, redrawTree} from "../DrawModes/DrawUtils";
+import {drawAtom, redrawProof, redrawTree} from "../DrawModes/DrawUtils";
 import {legalColor, illegalColor} from "../Themes";
 import {drawAltered, alterAtom, alterCutChildren} from "../DrawModes/EditModeUtils";
 import {isMoveLegal} from "./ProofMoveUtils";
@@ -92,28 +92,21 @@ export function proofMoveMultiMouseUp(event: MouseEvent) {
             event.x - startingPoint.x,
             event.y - startingPoint.y
         );
+        let tempNode: CutNode | AtomNode | null = null;
 
         if (currentNode instanceof CutNode) {
-            const tempCut: CutNode = alterCutChildren(currentNode, moveDifference);
-
-            if (isMoveLegal(currentProofTree, tempCut)) {
-                nextStep.tree.insert(tempCut);
-            } else {
-                nextStep.tree.insert(currentNode);
-            }
+            tempNode = alterCutChildren(currentNode, moveDifference);
         } else if (currentNode instanceof AtomNode) {
-            const tempAtom: AtomNode = alterAtom(currentNode, moveDifference);
-
-            if (isMoveLegal(currentProofTree, tempAtom)) {
-                nextStep.tree.insert(tempAtom);
-            } else {
-                nextStep.tree.insert(currentNode);
-            }
+            tempNode = alterAtom(currentNode, moveDifference);
         }
 
-        treeContext.proofHistory.push(nextStep);
-        redrawTree(nextStep.tree);
+        if (tempNode !== null && isMoveLegal(currentProofTree, tempNode)) {
+            nextStep.tree.insert(tempNode);
+            treeContext.proofHistory.push(nextStep);
+            redrawTree(nextStep.tree);
+        }
     }
+    redrawProof();
     legalNode = false;
 }
 

diff --git a/src/ProofTools/ProofMoveSingleTool.ts b/src/ProofTools/ProofMoveSingleTool.ts
@@ -9,7 +9,7 @@ import {AtomNode} from "../AEG/AtomNode";
 import {CutNode} from "../AEG/CutNode";
 import {treeContext} from "../treeContext";
 import {offset} from "../DrawModes/DragTool";
-import {drawCut, drawAtom, redrawTree} from "../DrawModes/DrawUtils";
+import {drawCut, drawAtom, redrawTree, redrawProof} from "../DrawModes/DrawUtils";
 import {legalColor, illegalColor} from "../Themes";
 import {alterAtom, alterCut} from "../DrawModes/EditModeUtils";
 import {ProofNode} from "../AEG/ProofNode";
@@ -74,7 +74,6 @@ export function proofMoveSingleMouseMove(event: MouseEvent) {
         //If the node is a cut, and it has an ellipse, make a temporary cut and draw that.
         if (currentNode instanceof CutNode) {
             const tempCut: CutNode = alterCut(currentNode, moveDifference);
-
             const color = isMoveLegal(currentProofTree, tempCut) ? legalColor() : illegalColor();
             drawCut(tempCut, color);
         } //If the node is an atom, make a temporary atom and check legality, drawing that.
@@ -100,30 +99,20 @@ export function proofMoveSingleMouseUp(event: MouseEvent) {
             event.x - startingPoint.x,
             event.y - startingPoint.y
         );
+        let tempNode: CutNode | AtomNode | null = null;
 
         if (currentNode instanceof CutNode) {
-            const tempCut: CutNode = alterCut(currentNode, moveDifference);
-
-            //If the new location is legal, insert the cut otherwise reinsert the cut we removed.
-            if (isMoveLegal(currentProofTree, tempCut)) {
-                nextStep.tree.insert(tempCut);
-            } else {
-                nextStep.tree.insert(currentNode);
-            }
+            tempNode = alterCut(currentNode, moveDifference);
         } else if (currentNode instanceof AtomNode) {
-            const tempAtom: AtomNode = alterAtom(currentNode, moveDifference);
-
-            //If the new location is legal, insert the atom, if not reinsert the atom we removed.
-            if (isMoveLegal(currentProofTree, tempAtom)) {
-                nextStep.tree.insert(tempAtom);
-            } else {
-                nextStep.tree.insert(currentNode);
-            }
+            tempNode = alterAtom(currentNode, moveDifference);
         }
 
-        treeContext.proofHistory.push(nextStep);
-        redrawTree(nextStep.tree);
+        if (tempNode !== null && isMoveLegal(currentProofTree, tempNode)) {
+            nextStep.tree.insert(tempNode);
+            treeContext.proofHistory.push(nextStep);
+        }
     }
+    redrawProof();
     legalNode = false;
 }
 

diff --git a/src/ProofTools/ProofResizeTool.ts b/src/ProofTools/ProofResizeTool.ts
@@ -9,7 +9,7 @@ import {AtomNode} from "../AEG/AtomNode";
 import {CutNode} from "../AEG/CutNode";
 import {treeContext} from "../treeContext";
 import {offset} from "../DrawModes/DragTool";
-import {drawCut, redrawTree} from "../DrawModes/DrawUtils";
+import {drawCut, redrawProof, redrawTree} from "../DrawModes/DrawUtils";
 import {legalColor, illegalColor} from "../Themes";
 import {ProofNode} from "../AEG/ProofNode";
 import {resizeCut} from "../DrawModes/EditModeUtils";
@@ -101,14 +101,12 @@ export function proofResizeMouseUp(event: MouseEvent) {
             if (tempCut.ellipse !== null) {
                 if (isLegal(tempCut)) {
                     currentProofTree.insert(tempCut);
-                } else {
-                    currentProofTree.insert(currentNode);
+                    treeContext.proofHistory.push(new ProofNode(currentProofTree, "Resize Cut"));
+                    redrawProof();
                 }
             }
         }
-
-        treeContext.proofHistory.push(new ProofNode(currentProofTree, "Resize Cut"));
-        redrawTree(treeContext.getLastProofStep().tree);
+        redrawProof();
         legalNode = false;
     }
 }