Add features: use goal count information printed at top of goals buffer in modeline, clear the goal window when proof is skipped (abort, admitted...).

ProofGeneral / PG

This repo is the new home of Proof General

https://proofgeneral.github.io

GNU General Public License v3.0

491 stars 88 forks source link

Add features: use goal count information printed at top of goals buffer in modeline, clear the goal window when proof is skipped (abort, admitted...). #755

Open axe1d opened 7 months ago

axe1d commented 7 months ago

In response to issues #605 and #168, I moved the information of current goal to the goals buffer modeline (to save some space and visibility basically), and cleared the goals buffer when encountering skip proof tactics like Abort. or Admitted. in Coq.

Matafou commented 7 months ago

The change is nice. A few remarks here and there. 2 questions:

should we remove the code that displays this information in the scritpting buffer then?
the coq-test-coqtop-unavailable.el fix seems unrelated but real. @hendriktews, @erikmd should we fix this?

axe1d commented 7 months ago

The change is nice. A few remarks here and there. 2 questions:

should we remove the code that displays this information in the scritpting buffer then?

the coq-test-coqtop-unavailable.el fix seems unrelated but real. @hendriktews, @erikmd should we fix this?

Thanks for your answer.

For the scripting buffer code process, my method is a bit messy but that was a first idea of solution. I parse the info from the goals buffer, move it to the modeline, and then create an overlay to make the info invisible in the buffer. I could dig more into code to outpass the intermediate processing.
For the coq-test-coqtop-unavailable.el test, that is totally unrelated, I just wanted to make sure the project was compiled on my config so I made it break. I should merge my commits for a cleaner PR. Don't hesitate if you have other advices of enhancement for this issue.

hendriktews commented 7 months ago

* the `coq-test-coqtop-unavailable.el` fix seems unrelated but real. @hendriktews, @erikmd should we fix this?

The error is related to this PR, it was introduced in the first commit f6a425f.

Matafou commented 7 months ago

The PR should first be cleaned up (useless files, then reduced to one commit imho.

axe1d commented 7 months ago

The PR should first be cleaned up (useless files, then reduced to one commit imho.

I thank you all for taking the time for reviewing my PR (which is my first ever, that's why it was a bit messy, and I apologize for that). I think it is a bit cleaner, and I welcome any advice on how to improve it before it can be merged (if it's needed of course).

hendriktews commented 7 months ago

I have the impression that the "clear goal window" part that is mentioned in the title of this PR is not present in the patch anymore. Can you confirm this? (I also suspect that this aspect did not work in your previous version, at least not for Admitted, as I don't remember that you have changed that the goals-reset-after-admitted is expected to fail, as it was before I merged PR #748 -- but I guess this suspicion is completely irrelevant now.)

hendriktews commented 7 months ago

I am not convinced every user will be fond of this change. The mode line is usually crowded and often it is truncated and some parts are not visible. Maybe this change should therefore be customizable, @erikmd @Matafou what is your opinion here?

Matafou commented 7 months ago

My opinion is that everything should be customizable, but I don't always apply it to myself. I think the current goal counter (on the scripting buffer) is not customizable either.

axe1d commented 7 months ago

Hi everyone, I modified my feature for Coq-only implementation, moved my functions to the coq subdir, and adapted the modeline update only when PG is instantiated for Coq. My goal here is to offer the possibility to users to custom the modeline as mentioned in #605. I thank you all again for this precise review of my code.

Matafou commented 2 months ago

I have been thinking about this PR a bit more and I think we should not merge it.

This feature (having the number of goals in the modeline) already exists: the number of goals is already printed in the modeline of the script buffer. If we want to move it to the goals buffer we should reuse and modify/clean/optionalize the existing code.

See https://github.com/ProofGeneral/PG/blob/734bcdb27fdcf54fbe6ab05bf957408e70c69748/coq/coq.el#L3121 and following, in particular the line:

(add-hook 'proof-shell-handle-delayed-output-hook #'coq-update-minor-mode-alist)

Feel free to submit a new PR adapting this part of the code.

The "clear buffer" stuff should go in a separate PR.

Remark on the code: Testing the name of the prover in the generic code is not the way PG is supposed to be configured. Specific provers should not appear in the generic part.

If noone object I shll close this PR soon.