proof-general narya-solve-hole function

[ElifUskuplu]

I used the changes in hole-offsets branch, edited the narya-handle-output and wrote narya-solve-hole function. I did not observe any error we received before, so I think it's better now.

What I've done :

• add narya-pending-hole-positions in order to store temporarily the hole positions when executing commands invisibly.

• edited narya-handle-output so that if called with an invisible command, store hole data in pending position instead of creating overlays immediately.

• created narya-solve-hole with the following properties:

  • When a hole created after a load (C-c C-n), use C-c C-SPC to enter the process
  • If the cursor is on a hole "?", then you will be asked to enter a term
  • If the term succeeds, namely; no error in solve %d := term command, then the hole will be replaced with (term). Putting parentheses is to avoid possible parsing problem. If we find a better way, we can edit this in the future.
  • Since the solve command is invisible during the process, we stored the data in pending hole positions. So in the case term includes new holes, we should store them in narya-hole again.
  • After processing all pending holes, narya-pending-hole-positions is cleared, ensuring no redundant data remains.

Let me know if you think it needs correction or more improvement.