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
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