Remove hypothesis display from goal list #962
Conversation
If the goals are displayed as collabsibles, only the first goal has its goal context (hypothesis) displayed.
Is this readable ? Should I also collapse them by default @ybertot ? |
|
This is what we are used to in PG, CoqIDE & co. |
|
Will it be possible to show the hypotheses again if we want? Like maybe by unfolding it? |
|
I thought I had answered one hour ago, but I would like to have the horizontal line displayed. |
|
Well, no, I don't know why I thought it was the habit in proof-general, but it is not. So as far as I am concerned, it is okay, but I think the question of Theo makes sense. |
I suppose I could put a collapsible for the hyps as well. Or add a button, but it will overload the UI a bit. Is it very useful ? |
|
Is the tab view displaying the whole context? If so maybe Theo prefers it |
|
I don't actually care much for the tab display and I think the current proposal is what I would like in most cases so maybe it's not such a necessity. |
|
If it is not too costly, I think a collapsible for the whole context would be good. |
I need more context.... |
|
Yes, I meant : make the whole sequence hyps for each goal collapsible. |
…text When a goal is expanded, a secondary action appears next to the collapse/expand button. This button represented by a closed/open eye allows to show/hide the goal context (hyps).
This is what I came up with. What do you guys think ? |
|
Sounds great! |
|
While you are at it, is it possible to avoid I mean, how many times do we want to tell the user the number of the goal? ;-) |
As many times as possible it turns out x-D #674 |
If the goals are displayed as collabsibles, only the first goal has its goal context (hypothesis) displayed.