Containers + bugfixes

[pimotte]

This PR supersedes both #80 and #82.

27eacbc...dev/variety-containers allows viewing the changes that are new with respect to those PRs.

Besides container support, this contains a slew of bugfixes related to the mapping, in particular, nodeUpdates and line number display.

• these bugs are both fixed
• these imports were fixed
• I removed the border of containers. I think it would be nice to show them in teacher mode, but in student mode is likely overkill. The pattern would be that the multilean correspond with exercises, we shouldn't span multilean over the entire document for elaboration reasons.

Testing

Edit both .mv and .lean documents, mainly focusing on inserting all nodes, wrapping/unwrapping input,hint and multilean.
Test in conjunction with the companion PR here: impermeable/waterproof-vscode#340

[DikieDick]

Wrapping the example in the following document in a multilean block does not seem to update the line number of the code cell inside.

import WaterproofGenre

#doc (WaterproofGenre) "Index" =>

::::multilean
\`\`\`lean
example : True := sorry
\`\`\`
::::

I think something like this for replaceAroundReplace would work (note that I return the update linedelta, but to my understanding this is not used anywhere:

replaceAroundReplace(step: ReplaceAroundStep, tree: Tree): ParsedStep {
        // We start by checking what kind of node we are wrapping with
        const wrappingNode = step.slice.content.firstChild;
        if (!wrappingNode) {
            throw new NodeUpdateError(" ReplaceAroundStep replace has no wrapping node ");
        }

        const pmSize = step.slice.size;
        if (pmSize != 2) throw new NodeUpdateError(" Size of the slice is not equal to 2 ");
        
        if (step.slice.content.childCount != 1) {
            throw new NodeUpdateError(" We only support ReplaceAroundSteps with a single wrapping node ");
        }

        // Check that the wrapping node is of a supported type (hint, input, or container)
        const insertedNodeType = wrappingNode.type.name;
        if (insertedNodeType !== "hint" && insertedNodeType !== "input" && insertedNodeType !== "container") {
            throw new NodeUpdateError(" We only support wrapping in hints, inputs, or containers ");
        }

        // If we are wrapping in a hint node we need to have a title attribute; container uses name attribute
        const title: string = insertedNodeType === "hint" ? wrappingNode.attrs.title
            : insertedNodeType === "container" ? wrappingNode.attrs.name
            : "";
        // Get the tags for the wrapping node
        const [openTag, closeTag] = this.nodeNameToTagPair(insertedNodeType, title);

        // The step includes a range of nodes that are wrapped. We use the mapping
        // to find the node at gapFrom (the first one being wrapped) and the node
        // at gapTo (the last one being wrapped).
        let nodesBeingWrappedStart = tree.findNodeByProsePos(step.gapFrom);
        const nodesBeingWrappedEnd = tree.findNodeByProsePos(step.gapTo);
        // If one of the two doesn't exist we error
        if (!nodesBeingWrappedStart || !nodesBeingWrappedEnd) throw new NodeUpdateError(" Could not find node in mapping ");
        
        ////// NEW ////////
        const openTagLines = countNewlines(openTag);
        const closeTagLines = countNewlines(closeTag);
        /////// END NEW ///////

        // findNodeByProsePos is biased: at a boundary position it returns the node ENDING there.
        // If gapFrom equals nodesBeingWrappedStart.pmRange.to, we got the preceding node instead
        // of the node that starts at gapFrom. Advance to the next sibling to correct this.
        if (nodesBeingWrappedStart.pmRange.to === step.gapFrom) {
            const parent = tree.findParent(nodesBeingWrappedStart);
            const siblings = parent ? parent.children : tree.root.children;
            const idx = siblings.indexOf(nodesBeingWrappedStart);
            if (idx + 1 < siblings.length) {
                nodesBeingWrappedStart = siblings[idx + 1];
            }
        }

        // Generate the document change (this is a wrapping document change)
        const docChange: WrappingDocChange = {
            firstEdit: {
                finalText: openTag,
                startInFile: nodesBeingWrappedStart.tagRange.from,
                endInFile: nodesBeingWrappedStart.tagRange.from,
            }, 
            secondEdit: {
                finalText: closeTag,
                startInFile: nodesBeingWrappedEnd.tagRange.to,
                endInFile: nodesBeingWrappedEnd.tagRange.to
            }
        };

        // We now update the tree

        const positions = {
            startFrom: nodesBeingWrappedStart.tagRange.from, 
            startTo: nodesBeingWrappedStart.tagRange.to,
            endFrom: nodesBeingWrappedEnd.tagRange.from,
            endTo: nodesBeingWrappedEnd.tagRange.to,
            proseStart: nodesBeingWrappedStart.pmRange.from,
            proseEnd: nodesBeingWrappedEnd.pmRange.to
        };
        
        const contentEnd = positions.endTo + openTag.length;
        const tagEnd = positions.endTo + openTag.length + closeTag.length;

        // Create the new wrapping node
        const newNode = new TreeNode(
            insertedNodeType,
            {from: positions.startFrom + openTag.length, to: contentEnd}, // inner range
            {from: positions.startFrom, to: tagEnd}, // full range
            title,
            positions.proseStart + 1, positions.proseEnd + 1, // prosemirror start, end
            {from: positions.proseStart, to: positions.proseEnd + 2}, // pmRange
            0
        );

        // We need to find the parent of the first node being wrapped
        const parent = tree.findParent(nodesBeingWrappedStart);
        if (!parent) throw new NodeUpdateError(" Could not find parent of nodes being wrapped ");

        const nodesInRange = tree.nodesInProseRange(positions.proseStart, positions.proseEnd);

        // Remove the nodes that are now children of the new wrapping node from their current parent
        nodesInRange.forEach(n => {
            parent.removeChild(n);
        });
        
        // Finally we need to update all nodes that come after the inserted wrapping node
        tree.traverseDepthFirst((thisNode: TreeNode) => {
            if (thisNode.pmRange.from >= positions.proseEnd) {
                thisNode.shiftOffsets(openTag.length + closeTag.length, 2);
                /////// NEW ////////
                thisNode.shiftLineStart(openTagLines + closeTagLines);
                /////// END NEW ///////
            }
        });

        // Now we need to insert the new wrapping node in the right place in the tree
        parent.addChild(newNode);
        
        nodesInRange.forEach(n => {
            newNode.addChild(n);
            n.shiftOffsets(openTag.length, 1);
            //////// NEW /////////
            n.shiftLineStart(openTagLines);
             ////// END NEW //////
        });

        tree.root.shiftCloseOffsets(openTag.length + closeTag.length, 2);

        return {result: docChange, newTree: tree, lineDelta: openTagLines + closeTagLines};
    }

[DikieDick]

Opinion: This extra padding is a bit ugly as it offsets the content further to the right. Can we make the distinction between container content and non container content visible in some other way? We could display an outline, but in teacher mode only? Do we really need to visually see where the containers are?

[pimotte]

Modified to show a light dashed line, only for teachers.

[pimotte]

Wrapping the example in the following document in a multilean block does not seem to update the line number of the code cell inside.

...

Fixed this along with the lifting case, which was also bugged.

[Tammo0987]

Should this todo be resolved here? I usually treat a todo as either solve it here, or put it in with an issue number, otherwise it should be just a plain comment I think.

[Tammo0987]

Also, technically not part of this PR, but this comment feels a bit weird as well.

[Tammo0987]

Should this be solved in this PR?

[pimotte]

Expanded comment to make it clearer. I think not, because I'm not sure if we will have containers that are nestable, and multilean is not.

[Tammo0987]

Also in this file, we introducing a lot of new references to the old coq/rocq name. I think we should avoid using the old term for code we change/update.

[pimotte]

So in this file I want to keep them for now, since these testcases (should) match what happens in actual files, and as of now, we still have the coq in the file format.

[pimotte]

@DikieDick I either fixed or addressed your and Tammo's comments, so I think this is ready for a final check:)