aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof.el
Commit message (Collapse)AuthorAge
* Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
|
* Fix incorrect assumption that noninteractive == byte-compilingGravatar Clément Pit--Claudel2017-03-08
| | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
* merge ProofTreeBranch into main trunk:Gravatar Hendrik Tews2012-01-03
| | | | | | | | | | | | | | | | - add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof
* Add keywords for possible benefit of finder package.Gravatar David Aspinall2009-12-01
|
* Clean compileGravatar David Aspinall2009-09-10
|
* Only show splash message if noninteractiveGravatar David Aspinall2009-09-07
|
* Remove load order tweak experimentGravatar David Aspinall2009-09-07
|
* Requires processed more often (experiment)Gravatar David Aspinall2009-09-07
|
* Clean whitespaceGravatar David Aspinall2009-09-05
|
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
|
* Use proof-auxmodes to load auxiliary modes properly when required.Gravatar David Aspinall2008-02-06
|
* Comments.Gravatar David Aspinall2008-01-15
|
* Many rearrangements for compatibility, efficient/correct compilation, ↵Gravatar David Aspinall2008-01-15
| | | | | | | namespaces fixes. pre-shell-start-hook: remove this, use default names for modes proof-compat: simplify architecture flags, use standard (featurep 'xemacs).
* Fixed something wrong. Probably a file missing (proof-system.el ?).Gravatar Pierre Courtieu2008-01-03
|
* Updated.Gravatar David Aspinall2007-12-14
|
* Add unload utility for developmentGravatar David Aspinall2007-08-14
|
* Documentation.Gravatar David Aspinall2005-05-17
|
* Add proof-thms-bufferGravatar David Aspinall2002-09-04
|
* Fix commentGravatar David Aspinall2002-07-16
|
* GPLGravatar David Aspinall2002-06-21
|
* Year changesGravatar David Aspinall2002-03-21
|
* CommentsGravatar David Aspinall2002-01-16
|
* Added proof-trace-buffer.Gravatar David Aspinall2001-12-10
|
* Add variable proof-previous-script-bufferGravatar David Aspinall2001-08-30
|
* Move autoloads loads to proof-site, invoke (proof-splash-message)Gravatar David Aspinall2001-05-16
|
* Extra arg to proof-splash-display-screen.Gravatar David Aspinall2000-05-11
|
* Fixup loading.Gravatar David Aspinall2000-05-09
|
* Removed autoloads, util functions.Gravatar David Aspinall2000-05-09
|
* Moved code into proof-system and proof-utils.Gravatar David Aspinall2000-05-05
|
* Added proof-assistant-keymap and commands for defining insert keys.Gravatar David Aspinall2000-05-02
|
* Helper macros.Gravatar David Aspinall2000-05-01
|
* Update copyright dates, comments.Gravatar David Aspinall2000-04-04
|
* Added return value for proof-shell-maybe-erase-response. Bug report msg.Gravatar David Aspinall2000-03-13
|
* Fix to warn function to use format args.Gravatar David Aspinall2000-03-08
|
* Add definition of warn function for FSF compatibility.Gravatar David Aspinall2000-02-28
|
* Attempted fix for thy-mode X-Symbol problems. Still buggy.Gravatar David Aspinall2000-01-12
|
* More docstring for proof-customize-toggle.Gravatar David Aspinall1999-11-24
|
* Docstrings.Gravatar David Aspinall1999-11-24
|
* Renamed proof-auto-delete-windows -> proof-delete-empty-windowsGravatar David Aspinall1999-11-22
|
* Fix so clicking on url works in bug reportGravatar David Aspinall1999-11-22
|
* Fix proof-try-require for FSF Emacs.Gravatar David Aspinall1999-11-19
|
* Moved response buffer code here.Gravatar David Aspinall1999-11-18
| | | | | Moved -output-fontify-toggle away. Made proof-switch-to-buffer more robust
* Name change proof-window-dedicated -> proof-dont-switch-windows.Gravatar David Aspinall1999-11-17
|
* Docstrings, bug report msg. Added proof-warn-if-unset.Gravatar David Aspinall1999-11-16
|
* Repaired FSF font-locking. Define toggler for output hilite enable.Gravatar David Aspinall1999-11-15
|
* Moved proof-switch-to-buffer here from proof-script.elGravatar David Aspinall1999-11-15
|
* Some new macros. FSF fix for font-lock. Failed attempt not to turn on ↵Gravatar David Aspinall1999-11-15
| | | | font-lock everywhere.
* Many robustness improvements for error and interrupt handling:Gravatar David Aspinall1999-11-14
| | | | | | | | | | | | - Introduce proof-shell-error-or-interrupt-seen flag set after an error or interrupt was seen (in fact, on every call to proof-release-lock). Examine it in proof-activate-scripting to see whether hooks succeeded in activating scripting. - Test in the shell filter for the lock being held yet nothing in the action list, and clear the lock if so. Gets rid of repetetive proof-shell-busy messages when the queue is empty (for errors during development, or nasty uses of C-g) - Add a timeout to proof-shell-wait (not used yet)
* proof-nested-goals-allowed -> proof-completed-proof-behaviourGravatar David Aspinall1999-11-14
| | | | | Patch for more flexible handling of closing goal...save regions after proof has been completed.
* Added new face for debug messagesGravatar David Aspinall1999-11-13
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 11:21:44 +0000