Collapsing and Expanding parts of Proof Tree

[Bram28]

Various issues here:

• icon needs updating
• arrows need to go straight
• node after collapsed nodes needs to go right after those collapsed nodes
• allow for collapsing parts of trees that already have collapsed nodes ... expanding should only expand last collapse ... it still show those previously collapsed nodes, rather than expand everything

[Bram28]

icon needs to be fast-forward icon (indicating multiple transitions)

icon goes between two board state nodes, and take up same room as normal transition node

icon can be green or red depending on whether all collapsed transitions are valid or not

[Bram28]

Better, but these things still need to be implemented:

icon needs to go between two board state nodes. If the user selects collapsing function when a board state is selected, the collapsing is applied to either the transition before or after the selected board state.

icon should take up same room as normal transition node, so board and transition nodes keep being lined up between different branches.

icon needs to be green or red depending on whether all collapsed transitions are valid or not (or yellow if not checked for validity)

[Bram28]

A few other possible features:

1. Allow the user to select two board-state nodes between which the collapse takes place. In fact, we could mandate the user to select two nodes, so that the collapsed transitions will indeed end up between two board-state nodes. If the user selects only 1 board-state node, then the collapse will go as far as possible, as it is currently implemented. But the user cannot select a transition node and then choose Collapse, just like Merge doesn;t work on selecting transition nodes.
2. Allow the user to collapse parts of tree that do contain branches ... this can be done if:

a. the different branches are later merged into the same one node. Indeed, the user could select that node, or the program can figure out that there is such a node.

b. all branches lead to a contradiction, and so the whole collapsed sub-tree leads to a contradiction.

1. Have a hierarchy of collapses, i.e. you can collapse part of a tree that already contains collapses. And when you expand the 'outer collapse', it still shows the 'inner' collapse (rather than expand everything).

[Bram28]

Here are some bugs:

1. The first merge should be placed more to the left: right after the right-most of the selected nodes, i.e. it should ignore other nodes (which apparently right now it doesn't). And as far as the y coordinate: it should be 'between' the selected nodes (either the average of all selected nodes ... or right between the 'highest' and 'lowest' of selected nodes).
2. The second merge ... is obviously misplaced!