The Coq mailing list

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

Others have asked for a progress indicator, too.

OK, I think these requests should keep me busy!

-- Paul

On Fri, Jun 17, 2016 at 1:34 PM, Jonathan Leivent 
<jonikelee AT gmail.com>
 wrote:
>
>
> On 06/17/2016 01:13 PM, Paul A. Steckler wrote:
>>
>> 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
>
>
> Certainly configurable.  In some cases, showing hyps that other hyps or the
> conclusion depend on is redundant, because it is trivial for the user to
> figure out their types from their uses.  Maybe if those hyps were just
> highlighted at their uses in some way - maybe a particular color to indicate
> that they are hyps and not global constants.
>
> However, because humans tend not to be as proficient at type inference as
> machines, there's probably some complexity such that merely highlighting a
> hyp at its usage and not dedicating a line to directly showing its type is
> annoying.  Maybe by having the mouse hover over the user click on a usage,
> that would bring up a tooltip with its type.  And clicking on the usage
> would make the line for that hyp visible.
>
> Maybe that tooltip could apply to evars as well.  And maybe clicking on an
> evar would show its goal.
>
>
>
> On a different front: how about a version of that new colorized progress bar
> that CoqIDE has at the bottom?
>
> -- Jonathan
>