aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-01-27added option -f FONT;Makarius Wenzel
2011-01-26ns-popup-font-panel: pass through argument list (used in Aquamacs Options menu).David Aspinall
2011-01-26Add autotest-start with debug for nowDavid Aspinall
2011-01-26Add autotest startDavid Aspinall
2011-01-26Add pg-autotest-start to allow debug startup, which doesn't catch errors.David Aspinall
2011-01-26- more info on the elements of proof-action-list; the COMMANDSHendrik Tews
list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert.
2011-01-26- fix 1 second problemHendrik Tews
- add limitations in the docs
2011-01-26- fix problem descriptionHendrik Tews
2011-01-25proof-deactivate-scripting: cleanup this function to make moreDavid Aspinall
intelligible, also to properly support behaviour needed for `proof-no-fully-processed-buffer'.
2011-01-25Remove semisDavid Aspinall
2011-01-25proof-fast-process-buffer: set to t also on Windows.David Aspinall
Untested, see http://proofgeneral.inf.ed.ac.uk/trac/ticket/308
2011-01-25Bump/relax version numbers. Error for <23, warning for minor version mismatch.David Aspinall
2011-01-25Remove debug messagesDavid Aspinall
2011-01-25- unlock files when retracting a Require command (implemented viaHendrik Tews
a span-delete-action and the 'coq-locked-ancestors property in the spans of Require commands)
2011-01-25Set version tag for new release.David Aspinall
2011-01-25Note recent changesDavid Aspinall
2011-01-25Remove dead codeDavid Aspinall
2011-01-25Remove proof-shell-wait that causes deadlock with new multiple-file code.David Aspinall
2011-01-25proof-shell-kill-function: use our own busy loop, as proof-shell-waitDavid Aspinall
expects normal prover IO. Addresses http://proofgeneral.inf.ed.ac.uk/trac/ticket/384
2011-01-25Dump *Messages* and *PG Debug* into log file, they have useful info.David Aspinall
2011-01-24- change 'span-delete-action in 'span-delete-actions, which isHendrik Tews
now a list of functions to be run when the span is deleted. Use span-add-delete-action to add a delete action.
2011-01-24Set version tag for new release.David Aspinall
2011-01-24Add News for 4.1David Aspinall
2011-01-23updated theory headers;Makarius Wenzel
2011-01-23TypoDavid Aspinall
2011-01-23Documentation updatesDavid Aspinall
2011-01-23proof-shell-exit: mention quit command and quit timeout in docDavid Aspinall
2011-01-23Make proof-shell-quit-timeout a prover-specific customize option, default to ↵David Aspinall
45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384.
2011-01-23proof-protected-process-or-retract: don't give failure error if nothing to doDavid Aspinall
Addresses Trac #383
2011-01-23Save the log file without querying user on exitDavid Aspinall
2011-01-23Kill prover process without asking on Emacs exitDavid Aspinall
2011-01-23Fix typoDavid Aspinall
2011-01-21- use time-less-pHendrik Tews
- delete previous-head, simplify loop - coq 8.2 compatibility - describe bug for killing completely asserted active buffers in coq/ex/test-cases/retract-completely-asserted
2011-01-19pg-create-in-span-context-menu: remove "Move up" and "Move down".David Aspinall
These don't seem to be very useful or reliable.
2011-01-19pg-show-all-portions: protect against empty hash tablesDavid Aspinall
2011-01-19Set version tag for new release.David Aspinall
2011-01-19Update date stampsDavid Aspinall
2011-01-19- switch off automatic compilation for coq to not surprise usersHendrik Tews
too much
2011-01-19- improved doc nodes Using file variables and Locking AncestorsHendrik Tews
2011-01-18- fixed stale load path problem with killing the proof shell inHendrik Tews
the deactivation-hook
2011-01-18- implemented coq-lock-ancestors as described in the docs alreadyHendrik Tews
2011-01-18Add multiple file test caseDavid Aspinall
2011-01-18Alternative fix to #382.David Aspinall
2011-01-18set proof-auto-action-when-deactivating-scripting to 'retract,David Aspinall
to stop new multiple file handling for Coq interactive queries
2011-01-18Localise compilation fix for dynamic scope of `queueitems\'.David Aspinall
2011-01-18- fixed compilation errorsHendrik Tews
2011-01-18- fix broken external compilationHendrik Tews
- fix quitting during compilation - substitute "compile" for "recompile" - added documentation
2011-01-18Removing a debugging message.Pierre Courtieu
2011-01-18Set version tag for new release.David Aspinall
2011-01-18Fix trac 382 by not setting save-abbrevs.Pierre Courtieu