The Coq mailing list

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

It would be straightforward to add a show-goal-on-hover feature to
Proof General.

I can add that to PG/xml, if anyone is interested.

On Wed, Aug 16, 2017 at 2:14 PM, James R Wilcox 
<jrw12 AT cs.washington.edu>
 wrote:
>> James, what tool did you use for you indeed awesome dep-destruct
>> webpage? The fact that the same goals-on-hover rendering does not
>> exist for your other posts (
>> https://homes.cs.washington.edu/~jrw12/SharedMem.html for example )
>> unfortunately suggests that there may be a fair amount of manual
>> effort involved.
>
>
>  There is indeed quite a bit of manual effort involved. I use this python
> script to process a coq file with special commands in comments. To get hover
> over, contexts must be manually inserted into commands in the coq file. I
> sometimes use an emacs macro to semi-automate this process, but it still
> requires keystrokes linear in the number of proof steps.
>
> I wish such trickery were not required, and would be happy to hear of better
> approaches.
>
> James