Show/hide of proofs in Coq can hide too much

[David Aspinall]

As on the subject line. Test case: example.v, click on Hide for the proof when the largest area is highlighted. There are probably too many underlying script elements.

[David Aspinall]

Note on what happens here with PG's attempt at code folding/hiding:

The too-large region easily hidden in example.v is actually the area corresponding to the Module which gets marked up as a proof span. It seems that this is selected before smaller regions which are underneath: the span-at function chooses at random. (This can be made better by using span-at before, although the sorting may be the wrong way round in that now --- can we instead simply find the right region based on what the mouse is highlighting?)

What should happen: for making something invisible, we take the visibility span which is controlled by the command span clicked on. The 'type labelled span (alone) should have the 'type property, and only non-overlapping spans have this property so they are unique. Goal-save regions corresponding to proofs encompass sequences of command regions inside.

Making things visible is more tricky. When we get a click, it cannot be inside an invisible region since the cursor moves across them without entering them. So instead we may use a heuristic to decide: if the cursor/click is next to an invisible region on either side, we make it visible.

Nested invisible elements are bound to be tricky unfortunately and this is what is happening with the Module level "proof" elements for Coq. To make this better we perhaps need to select the largest invisible region when we find one next to the cursor.

This is all a lot of effort for folding-like behaviour which could probably be better provided by CEDET or another mode.