The Coq mailing list

["Paul A. Steckler" <steck AT stecksoft.com>]

We might be able to do one or more of these, and we should discuss
when I'm farther along.

The XML protocol returns lists of goals, classified in various ways
(shelved, abandoned, background). The window size can be queried, so
the way goals are displayed can be cued from that.

What types of hypotheses would you like to hide, or would you want
that configurable in some way?

-- Paul



On Fri, Jun 17, 2016 at 12:47 PM, Jonathan Leivent 
<jonikelee AT gmail.com>
 wrote:
> Could PG be made to show multiple complete goals if the goal window is big
> enough?  I know there are various ways to ask for one or more goals to be
> shown, but this question is whether it is possible to do this automatically
> based on the size of the goal window.
>
> How about having a separate goal window for the current goal vs for the
> others?
>
> How about having a way to automatically show non-focused goals, as via Show
> Existentials, in a separate window?
>
> How about having a way to hide hypotheses based on type, or based on their
> being depended on in other hyps?  True - the current multiple-hyps-per-line
> is very nice, but it would be really nice if what I see in the goals window
> is just what I need to see (subject to choices) and room is not taken up by
> unimportant or redundant info.  Set Hyps Limit isn't discriminating.  Maybe
> have the goal window just show some tool-tip-able small icon to show where
> some invisible hyps are in the context?
>
>
> How about a real-time extraction window?  This was started, but not
> completed.  I think the last time I checked there were issues on the Coq
> side in that what it was sending was a non-optimized extraction - what the
> window showed was much larger/complex than what would be extracted via the
> Extraction command when the definition was finished.
>
>
> -- Jonathan
>