aboutsummaryrefslogtreecommitdiff
path: root/generic/proof.el
AgeCommit message (Collapse)Author
1998-10-27Temp disable splashDavid Aspinall
1998-10-27Begun work on clean byte compilation / clarifying interfaces.David Aspinall
1998-10-26Splash screen now works for FSFDavid Aspinall
1998-10-22Separated splash screen codeDavid Aspinall
1998-10-22Moved user options into proof-configDavid Aspinall
1998-10-22Split proof.el into proof-config.el, proof-script.el, proof-shell.elDavid Aspinall
1998-10-22renamed fume-match-find-next-function-nameThomas Kleymann
1998-10-22fixed bug in fume-match-find-next-function-nameThomas Kleymann
1998-10-21o Replaced proof-register-new-processed-file by -possibly-new- variant.David Aspinall
o Allowed proof-shell-process-file function to return nil o Fixed bug (missing declaration of 'file') in proof-shell-process-urgent-message
1998-10-21no longer displays important messages about file assertion/retractionThomas Kleymann
1998-10-21Improved maintainability of code in proof-check-process-available.David Aspinall
1998-10-21fixed a bug in `proof-check-process-available'Thomas Kleymann
1998-10-21o made buffer-file-truename even saferThomas Kleymann
o fixed bug in ...-check-...
1998-10-21o Improved error messagesThomas Kleymann
o Fixed bug in proof-toolbar-next
1998-10-21Added code to register fully processed file. Multiple file fix list updatedDavid Aspinall
1998-10-21Changed from forcing w3 to using customizable browse-urlDavid Aspinall
1998-10-21Added proof-activate-scripting-hook and fixed regexpsDavid Aspinall
1998-10-20Changed minibuffer tag to have name of prover instead of ProofDavid Aspinall
1998-10-19Bug fixes for multiple file code, da/tms.David Aspinall
1998-10-18support for nested goals is now restricted to CoqThomas Kleymann
1998-10-18Reimplemented multiple file proof developmentsThomas Kleymann
1998-10-13Disabled font-lock in process bufferThomas Kleymann
1998-10-12Added compatibility hack for customize-menu-create.David Aspinall
1998-10-12Added sensible error message for attempting undo on empty locked region.David Aspinall
1998-10-12Made defface's work for dark background Emacsen (default for FSF on Linux).David Aspinall
1998-10-12Dox. Made proof-shell-exec-loop not complain about empty action list.David Aspinall
1998-10-12Splash screen tries gif if jpeg not available. Using hack by tmsDavid Aspinall
1998-10-12Fixed typo.David Aspinall
1998-10-12Toolbar featurep. Separate Internals menu. Doc strings.David Aspinall
1998-10-09Customize group name: prover-config, not proof-config.David Aspinall
1998-10-09Minor bug fixes, code, doc improvements.David Aspinall
1998-10-08Changed binding for C-c RETDavid Aspinall
1998-10-07Added more documentation.David Aspinall
Made new proof-config customization group for variables supposed to be configured by prover specific settings (as opposed to user options, which are set by users). This adds type information and useful facility for testing new instances of PG. Similarly added proof-shell customization group. Removed (what I assume to be) defunct variables proof-post-shell-exit-hook, proof-shell-echo-input. Made deflocal do 'setq-default', not 'setq'. (I consider this a bugfix, but no calls to deflocal use other than nil value anyway, so this bug had no effect.) Added code for displaying splash screen. Attempted fix for proof-issue-new-command when process inactive. Improved functions proof-script-new-command-advance, proof-script-next-command-advance, called from proof-assert-next-command.
1998-10-05da> BTW, the menus have disappeared!Thomas Kleymann
They are back courtesy of reintroducing an easy-menu-add call.
1998-10-02Moved menu definition back into proof-config-done.David Aspinall
1998-10-02added LEGO support for proof-goal-command and proof-save-commandThomas Kleymann
1998-10-01Updated maintainer tags to remove lego email address.David Aspinall
1998-10-01Added docstrings and comments.David Aspinall
Removed last of "not authorized for this documentation" nonsense. Replaced constant string "COMMENT" by proof-no-command. Begun work on new functions: proof-{next,previous}-matching-command. Work on proof-issue-goal, proof-issue-save (rough edges left as FIXMEs).
1998-09-23Changed customization group and removed nagging not-busy error messageDavid Aspinall
1998-09-22Cleaned up and improved some code, added docstrings, FIXMEs.David Aspinall
Added proof-issue-goal and proof-goal-command. Rearranged to get ready for splitting into proof-script and proof-shell. Added proof-one-command-per-line user option.
1998-09-17Fix in proof-shell-handle-outputDavid Aspinall
1998-09-17fixed a bug in proof-shell-filter and proof-shell-handle-ouputThomas Kleymann
1998-09-16Moved proof-info-dir into proof-site and defcustom'd it.David Aspinall
Set the Info directory list there rather than after proof.el has loaded. Add the proof-info-dir onto the end of Info-default-directory-list, not the start.
1998-09-16fixed implementation fo proof-find-next-terminator;Thomas Kleymann
it can now be used even when there is no corresponding proof process
1998-09-16Improved doc. Removed proof-mode-version-string.\nMade ↵David Aspinall
proof-prog-name-ask-p defcustom
1998-09-15Reimplemented proof-shell-popup-eager-annotationThomas Kleymann
These are no longer displayed in the *GOALS* buffer.
1998-09-14Added docs and proof-restart-script-same-process (may need work)David Aspinall
1998-09-10-Added documentationThomas Kleymann
-Simplified code for setting faces -Reimplimented `proof-shell-handle-error' -Improved `proof-shell-filter'; it no longer removes the prompt annotation -The Shell no longer automatically scrolls to the end (or so I hope)
1998-09-09Made proof-assert-next-command move forward by default.David Aspinall
1998-09-09Added Id to headers.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:35:13 +0000