David Aspinall <david.aspin...@ed.ac.uk> writes:

   I suggest refactoring the setting of prog-command-line in
   proof-shell-start into a new function which does this, so
   (proof-shell-prog-command-line) returns the command line you want.
   That would clear up the beginning of proof-shell-start a bit.

I made a simple change to get the functionality I need for coq.
The initialization of prog-name-list1 is now

              (if (functionp (proof-ass-sym prog-args))
                  ;; complex assistants define <PA>-prog-args as function
                  ;; that computes the argument list.
                  (cons proof-prog-name (funcall  (proof-ass-sym prog-args)))
                (if (proof-ass prog-args)
                    ;; Intermediate complex assistants set the value
                    ;; of <PA>-prog-args to the argument list.
                    (cons proof-prog-name (proof-ass prog-args))
                  ;; Trivial assistants simply set proof-prog-name
                  (split-string proof-prog-name)))

This is, however, not the expected simplification. I decided for
this simple change, because it keeps the functionality of other
proof assistants without that I have to touch their code.


ProofGeneral-devel mailing list

Reply via email to