proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2009-09-09	Prevent font-lock in shell by altering font-lock-global-modes locally	David Aspinall

2009-09-09	Clear shell buffer contents on restart.	David Aspinall
	proof-shell-classify-output-system-specific -> proof-shell-handle... and simplify system specific hook. Repair error handling for Isabelle (search forward for matches) Add proof-shell-font-lock-keywords.
2009-09-09	Simplify output processing; delay some goals/response classification	David Aspinall
	until postponed goals/response output drawn. Remove some internal variables. Slightly generalise message model to include Coq 8.1's MESSAGE GOALS output form. Improve documentation of proof-shell-filter and friends to explain this.
2009-09-08	proof-shell-handle-error-output: renamed, and simplified	David Aspinall
	to use suggestion to take message from `proof-shell-last-output', now that is no longer munged to remove markup.
2009-09-07	Whitespace	David Aspinall

2009-09-06	Make sure proof-shell-last-output, proof-shell-last-prompt and	David Aspinall
	proof-shell-delayed-ouput remain non-nil.
2009-09-06	Reorganisation to avoid generating many intermediate strings from	David Aspinall
	the shell buffer, and match shell regexp directly inside it. This changes the types of several configuration settings. Also some improvements to scomint configuration and changes to proof-shell-exec-loop to send the next command to the prover before starting to process the output from the last. This reorganisation is still in testing and will take time to bed down.
2009-09-05	Clean whitespace	David Aspinall

2009-09-04	replace-in-string -> replace-regexp-in-string	David Aspinall

2009-09-04	Define a cleanup function to run intermittently or by hand, avoiding ↵	David Aspinall
	pg-remove-specials.
2009-09-04	Remove proof-shell-prompt-pattern, no longer used.	David Aspinall

2009-09-04	Require on scomint in right place	David Aspinall

2009-09-04	Possible bug in interrupt signaling discovered	David Aspinall

2009-09-04	Use scomint instead of comint	David Aspinall

2009-09-03	Shorten startup message	David Aspinall

2009-08-28	Fix compile warnings	David Aspinall

2009-08-20	Doc tweaks via checkdoc.	David Aspinall

2009-08-20	Documentation improvements.	David Aspinall
	Experiment with `process-adaptive-read-buffering' Do not run `proof-shell-insert-hook' if input string is empty or single CR.
2009-08-19	proof-shell-insert: add scriptspan argument, to pass source positions to ↵	David Aspinall
	proof-shell-insert-hook
2009-08-17	Move proof-interrupt-process to proof-shell. Add pending interrupt ↵	David Aspinall
	behaviour. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/179
2009-08-14	Start refactoring to support more sophisticated queue handling, by adding ↵	David Aspinall
	flags to proof action list
2009-08-07	rename: proof-full-decoration -> proof-full-annotation	David Aspinall

2009-05-27	Cleanup more Emacs compatibility	David Aspinall

2009-05-26	Add proof state hover messages to proof script, along with useful customization.	David Aspinall

2009-05-26	Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor ↵	David Aspinall
	cleanups
2009-03-31	recovered proof-shell-process-urgent-message, by re-introducing ↵	Makarius Wenzel
	commented-out parenthesis and refreshing formerly unreachable cases;
2008-08-03	Disable subterm markup removal	David Aspinall

2008-07-24	Merge changes from Version4Branch.	David Aspinall

2008-07-10	Minimal patch for Sledgehammer problem with Isabelle.	David Aspinall
	Credit due to Makarius. Tested very briefly with Coq. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/200
2008-02-06	Use proof-auxmodes to load auxiliary modes properly when required.	David Aspinall

2008-01-30	Fix RCS tags	David Aspinall

2008-01-30	Comment cleanups. buffer-substring -> buffer-substring-no-properties.	David Aspinall
	Make proof-shell-handle-output robust against START-REGEXP match fail (can happen if shell buffer is garbled/user-edited). Make proof-shell-insert robust against null STRING (should not happen; development artefact while getting rid of proof-no-command). Update date.
2008-01-28	Add hooks for unicode tokens within proof shell	David Aspinall

2008-01-25	split string on proof-rsh-command	David Aspinall

2008-01-16	Reduce compiler warnings. Minor fixes.	David Aspinall

2008-01-16	Compilation tweaks	David Aspinall

2008-01-16	Cleanup compile	David Aspinall

2008-01-15	Before calling pg-response-display-with-face, strip eager annotation but not ↵	David Aspinall
	specials.
2008-01-15	Fix cleaning minibuffer echo of urgent messages when proof-shell-unicode is ↵	David Aspinall
	set. Cleanup comments.
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).
2007-12-14	Cleanup coding system setting, comments	David Aspinall

2007-12-14	Add proof-shell-set-text-representation to disable multibyte characters in ↵	David Aspinall
	legacy case. Use proof-shell-unicode to control whether bytes 128-255 are stripped from output.
2007-12-14	Munging with input/output encoding; try to make consistent.	David Aspinall

2007-12-14	Tune some comments. Remove annotations in processed text from	David Aspinall
	shell buffer. Supports copy-and-paste, fixing trac #112.
2007-12-13	Remvoe typo	David Aspinall

2007-12-13	Comment the removal of the call to toggle-enable-multibyte-characters.	David Aspinall

2007-12-12	Compatibility with coq trunk where some special symbols are removed.	Pierre Courtieu

2007-08-19	proof-append-alist: detach queue span if no commands after comments stripped.	David Aspinall
	Fixes trac report #138: processing comments alone leads to spurious read-only region.
2007-05-10	Patch for utf-8 test	David Aspinall

2006-09-22	Cut comint input ring, minor efficiency tweak.	David Aspinall