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
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.
This sounds wise, and what Pierre originally suggested, although if I've
followed it seems as if that's
David Aspinall david.aspin...@ed.ac.uk writes:
So, yes, you may need to adjust the load path manually with
the scriting activate/deactivate hooks.
Undoing those Add LoadPath commands with Remove LoadPath commands
would be rather difficult. If one adds a directory which is
already in the
Undoing those Add LoadPath commands with Remove LoadPath commands
would be rather difficult. If one adds a directory which is
already in the LoadPath, coq reorders the LoadPath, a subsequent
remove will not yield the starting state.
In that case I'm not sure how you can achieve what you need,
2011/1/13 Pierre Courtieu pierre.court...@cnam.fr
This is not entirely true. The backtrack mechanism of coq/pg is more robust
than that, thanks to state numbers of coq you can undo most invisible
commands by going back to a point in the file that was scripted before the
invisble command.
Pierre Courtieu pierre.court...@cnam.fr writes:
invisble command. However LoadPath is probably not part of the undo model
and Coq does not retract them when going back to a previous state.
I just tried, changes in the LoadPath are not undone by
Backtrack. This basically means that when
For getting correct multiple file scripting for coq I would first
try to restart coqtop on every new scripting buffer. What would
be the best way to achieve this? Put proof-shell-exit into
proof-deactivate-scripting-hook?
I suppose but this does seem pretty crude, there is some cost to
Pierre Courtieu pierre.court...@cnam.fr writes:
2011/1/13 David Aspinall david.aspin...@ed.ac.uk
I suppose Pierre means that you need a way to influence the command line
calculation as you wanted, perhaps with yet another control function/hook
or
variable for prog-args (already
Hi,
I just noticed the following effect: When I send commands with
proof-shell-invisible-command from a member of
proof-activate-scripting-hook, then these commands are not
automatically retracted changing the scripting buffer.
Is this really a feature? Do I have to add a corresponding
