Open calintat opened 1 year ago
If we do this, I think it makes sense to ellipsis-ise diagrams too, beyond the render size; e.g. if we don't draw up to the boundary of the diagram, we should draw the visual equivalent of ...
so that it's possible to distinguish between boundary vs not rendered.
If you have a large diagram (like some of Manuel's proofs which have over 1000 slices), it makes no sense to render the entire diagram as you cannot realistically view the entire thing. This also makes it really hard to do any simplifications as after every contraction or expansion we have to re-render the whole diagram even though you're only looking at a few slices.
So Manuel and I were thinking we should have some kind of "peephole view" into the diagram where you can only view K slices of the diagram at a time for some number K. For large diagrams (i.e. of size more than K) this should be enabled by default.
In terms of UI, I was thinking we could have a slider under the path control where you can choose the subset of the diagram's slices that you want to view. Maybe we could use the page up / page down keys to control this.
This also makes a lot of sense for the 4D view. Realistically I don't think we can ever render a diagram with 1000 slices as a movie, but we could render it in fragments. Maybe we could integrate the UI above with the existing scrub control for 4D.