| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2012-01-03 | merge ProofTreeBranch into main trunk: | Hendrik Tews | |
| - 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 | |||
| 2009-12-01 | Add keywords for possible benefit of finder package. | David Aspinall | |
| 2009-09-10 | Clean compile | David Aspinall | |
| 2009-09-07 | Only show splash message if noninteractive | David Aspinall | |
| 2009-09-07 | Remove load order tweak experiment | David Aspinall | |
| 2009-09-07 | Requires processed more often (experiment) | David Aspinall | |
| 2009-09-05 | Clean whitespace | David Aspinall | |
| 2008-07-24 | Merge changes from Version4Branch. | David Aspinall | |
| 2008-02-06 | Use proof-auxmodes to load auxiliary modes properly when required. | David Aspinall | |
| 2008-01-15 | Comments. | David Aspinall | |
| 2008-01-15 | Many rearrangements for compatibility, efficient/correct compilation, ↵ | David Aspinall | |
| namespaces fixes. pre-shell-start-hook: remove this, use default names for modes proof-compat: simplify architecture flags, use standard (featurep 'xemacs). | |||
| 2008-01-03 | Fixed something wrong. Probably a file missing (proof-system.el ?). | Pierre Courtieu | |
| 2007-12-14 | Updated. | David Aspinall | |
| 2007-08-14 | Add unload utility for development | David Aspinall | |
| 2005-05-17 | Documentation. | David Aspinall | |
| 2002-09-04 | Add proof-thms-buffer | David Aspinall | |
| 2002-07-16 | Fix comment | David Aspinall | |
| 2002-06-21 | GPL | David Aspinall | |
| 2002-03-21 | Year changes | David Aspinall | |
| 2002-01-16 | Comments | David Aspinall | |
| 2001-12-10 | Added proof-trace-buffer. | David Aspinall | |
| 2001-08-30 | Add variable proof-previous-script-buffer | David Aspinall | |
| 2001-05-16 | Move autoloads loads to proof-site, invoke (proof-splash-message) | David Aspinall | |
| 2000-05-11 | Extra arg to proof-splash-display-screen. | David Aspinall | |
| 2000-05-09 | Fixup loading. | David Aspinall | |
| 2000-05-09 | Removed autoloads, util functions. | David Aspinall | |
| 2000-05-05 | Moved code into proof-system and proof-utils. | David Aspinall | |
| 2000-05-02 | Added proof-assistant-keymap and commands for defining insert keys. | David Aspinall | |
| 2000-05-01 | Helper macros. | David Aspinall | |
| 2000-04-04 | Update copyright dates, comments. | David Aspinall | |
| 2000-03-13 | Added return value for proof-shell-maybe-erase-response. Bug report msg. | David Aspinall | |
| 2000-03-08 | Fix to warn function to use format args. | David Aspinall | |
| 2000-02-28 | Add definition of warn function for FSF compatibility. | David Aspinall | |
| 2000-01-12 | Attempted fix for thy-mode X-Symbol problems. Still buggy. | David Aspinall | |
| 1999-11-24 | More docstring for proof-customize-toggle. | David Aspinall | |
| 1999-11-24 | Docstrings. | David Aspinall | |
| 1999-11-22 | Renamed proof-auto-delete-windows -> proof-delete-empty-windows | David Aspinall | |
| 1999-11-22 | Fix so clicking on url works in bug report | David Aspinall | |
| 1999-11-19 | Fix proof-try-require for FSF Emacs. | David Aspinall | |
| 1999-11-18 | Moved response buffer code here. | David Aspinall | |
| Moved -output-fontify-toggle away. Made proof-switch-to-buffer more robust | |||
| 1999-11-17 | Name change proof-window-dedicated -> proof-dont-switch-windows. | David Aspinall | |
| 1999-11-16 | Docstrings, bug report msg. Added proof-warn-if-unset. | David Aspinall | |
| 1999-11-15 | Repaired FSF font-locking. Define toggler for output hilite enable. | David Aspinall | |
| 1999-11-15 | Moved proof-switch-to-buffer here from proof-script.el | David Aspinall | |
| 1999-11-15 | Some new macros. FSF fix for font-lock. Failed attempt not to turn on ↵ | David Aspinall | |
| font-lock everywhere. | |||
| 1999-11-14 | Many robustness improvements for error and interrupt handling: | David Aspinall | |
| - 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) | |||
| 1999-11-14 | proof-nested-goals-allowed -> proof-completed-proof-behaviour | David Aspinall | |
| Patch for more flexible handling of closing goal...save regions after proof has been completed. | |||
| 1999-11-13 | Added new face for debug messages | David Aspinall | |
| 1999-11-12 | Notes about font-lock management. | David Aspinall | |
| 1999-11-12 | Fixes for response buffer display, x-symbol, output formatting. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |