search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

(RFC) Use an 'urgency' flag to decide whether to pop-up the goals buffer #122

Closed mtzguido closed 3 years ago

mtzguido commented 3 years ago

Hi Clément,

with @R1kM and others we were finding the fact that the goals buffers always opens up on a tactics error a bit annoying (especially when many buffers are open). So I came up with this patch to decide whether to display it or not. The idea is that F* provides and "urgency" level for each proofstate (currently just 0 or 1), and emacs will only pop-up the buffer when it is 1 (but will always log the error in the buffer). The urgency is 1 by default to not affect the old behavior.

Does this look sensible to you? I would imagine there's probably better ways to do it :-)

(F* master doesn't pass the urgency field yet, guido_tactics does).

mtzguido commented 3 years ago

Thanks Clément, much appreciated! I'll update this soon.

mtzguido commented 3 years ago

Just updated the PR according to your comments, let me know if I messed something up :). Also used if-let as you mentioned in the other (already merged) PR. Thanks a lot!

mtzguido commented 3 years ago

Thanks Clément! I cleaned it up a bit and rebased.