Ellipsis

[rtetley]

For larger goals, add an ellipsis mechanism. This leverages a depth parameter -> if depth of element > maxDepth then ellide. On top of that, boxes now have an included collapse, or expand mechanism.

[rtetley]

ping @gares @ybertot

[ybertot]

How does it get triggered? If it is enough to click on a sub-expression to have it collapse/expand, I think this is too obtrusive. It should be an action that can be easily triggered, but not too easily.

[gares]

Wow!

One thing to think about is what happens when the goal changes.

I agree about the clicking. I think we should come up with a list of actions (considering future work) and then decide what goes to a simple click and what requires a modifier or a dedicated contextual panel/menu.

I can recall a few ideas (from the past), but I'm sure there are more:

• alternative display for a notation, eg a = b vs a =_nat b, or just a + b vs addn a b
• about a symbol (like in the text buffer)
• jump to def (as above)
• apply tactic (eg. simpl or set) to the selected subterm

Anyway, hiding too-large terms and having a click on "..." expand a few levels more seems something that can be immediately useful. All the rest may need a bit more thinking.

[rtetley]

Just added a feature so that the hover effect (dashed line) and the click only work if you are pressing the 'Alt' key.