diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-11 18:28:27 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-11 18:28:27 +0000 |
| commit | b579b8930f4fa70d50d1934a9a96871d2e8d9fae (patch) | |
| tree | 393983ae9b169f42eec7f18522b9cafdf7fce3a1 /configure | |
| parent | d30331a104a066e3c16516b2c09b8493df767554 (diff) | |
Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820
This provides an ad-hoc way to solve the second part of
bug #2820 (Show Script not working when proof started inside a Load)
When doing Load on a file, two behaviors are possible:
- either the history stack is grown by only one command,
the "Load" itself. This is mandatory for command-counting
interfaces (CoqIDE).
- either each individual sub-commands in the file is added
to the history stack. This allows commands like Show Script
to work across the loaded file boundary (cf. bug #2820).
Ideally, we should be able to combine someday the benefits of
the two approaches. But in the meantime, we resort to a flag :
using "Unset Atomic Load" should make "Show Script" work across Load.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15601 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
0 files changed, 0 insertions, 0 deletions