aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-09-08Remove some spacesDavid Aspinall
2009-09-08Remove more of 80 codeDavid Aspinall
2009-09-08Updated.David Aspinall
2009-09-08proof-kill-goal-command: default to nil, not empty stringDavid Aspinall
2009-09-08Simplify coq-find-and-forget and drop v80 versionDavid Aspinall
2009-09-08Remove system-specific code as message before goals handled in core now. ↵David Aspinall
Alter proof-shell-start-goals-regexp to work in buffer.
2009-09-08CommentsDavid Aspinall
2009-09-08Update, remove proof-shell-abort-goal-regexpDavid Aspinall
2009-09-08Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵David Aspinall
LEGO messages)
2009-09-08More text about Unicode TokensDavid Aspinall
Remove proof-shell-abort-goal-regexp
2009-09-08CommentsDavid Aspinall
2009-09-08Oops: repair hybrid output broken by two window fix! See trac #109.David Aspinall
2009-09-08byte-compile-and-load on write is a bit too enthusiasticDavid Aspinall
2009-09-08Repair two-window working mode for when Coq doesn't produce hybrid output.David Aspinall
Print Proof -> just Print in context menu. Temporarily inhibit read only in response buffer for error highlighting. Reduce time for error highlighting
2009-09-08Clarify requireDavid Aspinall
2009-09-08Require on scomintDavid Aspinall
2009-09-08proof-shell-handle-error-output: renamed, and simplifiedDavid Aspinall
to use suggestion to take message from `proof-shell-last-output', now that is no longer munged to remove markup.
2009-09-08Fix docstrings, remove spurious nullDavid Aspinall
2009-09-08pg-response-display-with-face: remove update of `proof-shell-last-output'David Aspinall
2009-09-08Remove use of regexp-opt-depth and clarify doc ofDavid Aspinall
`unicode-tokens-token-match-regexp'. Fix typo in `proof-tactical-name-face'.
2009-09-08Remove devel. from testall targetDavid Aspinall
2009-09-08Remove warnings in batch compile about functions possibly undefined atDavid Aspinall
runtime. Most of these are spurious (come from autoloads; byte comp seems to give these higher priority than declarations in same file).
2009-09-07Only show splash message if noninteractiveDavid Aspinall
2009-09-07Remove load order tweak experimentDavid Aspinall
2009-09-07Nuke spurious warningDavid Aspinall
2009-09-07Update autoloadsDavid Aspinall
2009-09-07Fix proof-shell-trace-output-regexp: match on annotation \^AI now tooDavid Aspinall
2009-09-07Deleted fileDavid Aspinall
2009-09-07Require unicode-tokens during compile.David Aspinall
2009-09-07scomint-check-proc: make defsubstDavid Aspinall
2009-09-07Attempt to handle splash buffer cleanly.David Aspinall
2009-09-07Revert change in 10.26 to use defpacustom after all, this givesDavid Aspinall
the prover-specific menu entry automatically. Fix compiler warning with a defvar.
2009-09-07Fix initialisation of isar-use-find-theorems-form in compiled file.David Aspinall
2009-09-07require proof-site also at startupDavid Aspinall
2009-09-07lego-shell-process-output -> lego-shell-classify-outputDavid Aspinall
2009-09-07Requires processed more often (experiment)David Aspinall
2009-09-07Fix compiler warningsDavid Aspinall
2009-09-07isar-use-find-theorems-form: use defcustom, not defpacustomDavid Aspinall
isar-keywords-name: fix custom group
2009-09-07Fix compiler warningsDavid Aspinall
2009-09-07Fix compiler warnings.David Aspinall
2009-09-07Isabelle->isabelle binary. Remove Isar homepage.David Aspinall
2009-09-07Don't try to compile obsolete twelf Emacs code.David Aspinall
2009-09-07Update for 4.0 and shorten.David Aspinall
2009-09-07(C) dateDavid Aspinall
2009-09-07Fix compile warnings and ensure compiled code behaves as expected.David Aspinall
2009-09-07Fix compile warning, rearrange docsDavid Aspinall
2009-09-07Require cl for compilation. Rearrange docs.David Aspinall
2009-09-07Attempt byte compilation only for emacs lisp!David Aspinall
2009-09-07isar-preprocessing: remove unnecessary save-match-data.David Aspinall
Fix a compile warning.
2009-09-07Remove \t in \<inverse> expansion.David Aspinall
Make \<spacespace> be a single EM-DASH SPACE
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-31 19:07:49 +0000