2002-07-01 David Aspinall * html/news.html: Syntax error * doc/ProofGeneral.texi, doc/PG-adapting.texi: Updates for 3.4 * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/news.html: Fix date on news item * generic/proof-utils.el: Use executable-find * generic/proof-script.el: proof-restart: also remove idiom internal spans. * generic/proof-x-symbol.el: Fix problem with GNU Emacs support: switch to multibyte in output buffers * isa/x-symbol-isabelle.el: Doc difference between isa and isar, fix prob with isa support. * isa/isabelle-system.el: Added isabelle-load-isar-keywords mimic of script startup. * isar/isar-syntax.el: Adjust syntax tables. * isar/isar.el: Adjust load order, and try to load a good isar-keywords file. Add several FIXMEs. * isar/test.el: Add code to test new parser. 2002-06-30 David Aspinall * isar/isar-keywords.el: Revert to previous version. Explain existence of other versions 2002-07-01 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/news.html: Fix date on news item * generic/proof-utils.el: Use executable-find * generic/proof-script.el: proof-restart: also remove idiom internal spans. * generic/proof-x-symbol.el: Fix problem with GNU Emacs support: switch to multibyte in output buffers * isa/x-symbol-isabelle.el: Doc difference between isa and isar, fix prob with isa support. * isa/isabelle-system.el: Added isabelle-load-isar-keywords mimic of script startup. * isar/isar-syntax.el: Adjust syntax tables. * isar/isar.el: Adjust load order, and try to load a good isar-keywords file. Add several FIXMEs. * isar/test.el: Add code to test new parser. 2002-06-30 David Aspinall * isar/isar-keywords.el: Revert to previous version. Explain existence of other versions * README: Update version * CHANGES: Update, cleanup * BUGS: Reorg. Mention fontification bug. * pgkit/README: New files. * generic/proof-script.el: Fix error catching in proof-deactivate-scripting-auto. * generic/proof-splash.el: Robustify form GNU Emacs * isa/x-symbol-isabelle.el: Fix x-symbol-isabelle-input-token-grammar to remove spurious backslashes * isa/isa-syntax.el: Fix GNU Emacs/X-Symbol compatibility for sml-sym-face added by Lucas Dixon. * etc/isar/Persistent.thy: New files. * generic/proof-script.el, generic/proof-shell.el: When killing process or scripting buffer, register file if it is complete, rather than always retracting. * generic/proof-shell.el: proof-shell-kill-function: deactivate scripting before shutting down prover 2002-06-24 David Aspinall * generic/proof-x-symbol.el: Require x-symbol-vars as recommended for new version (works with old too?) * generic/proof-menu.el: Disable fly past comments for old parser again. * generic/proof-config.el: Default to using old parser for now. * generic/proof-config.el, generic/proof-script.el: use-old-parser setting replaces use-new-parser setting [WARNING: big change] * generic/proof-compat.el: Also use our own buffer-syntactic-context in XEmacs 21.4. * isa/Example.ML, isa/Example.thy: Add Emacs mode comments at top * isa/thy-mode.el: Move auto-mode-alist hack here now Isar is default. * isa/isa.el: Fix comment * isa/x-symbol-isabelle.el: [TESTING] support for latest version of X-Symbol (back compat broken). * isa/isabelle-system.el: Hack to avoid loading x-symbol-isabelle * isar/isar-keywords.el: Fix to prevent {* being considered a command, flag edits * isar/isar.el: Remove auto-mode-alist hack, and require on x-symbol-isabelle [TESTING]. 2002-06-21 David Aspinall * FAQ: Wrong: mustn't delete isa dir, files shared with isar. * twelf/twelf.el, lego/lego.el, lego/lego-syntax.el, lego/x-symbol-lego.el, isar/isar.el, isar/isar-syntax.el, isa/x-symbol-isabelle.el, isa/isa.el, isa/isa-syntax.el, isa/thy-mode.el, acl2/acl2.el, html/download.html: GPL update * doc/PG-adapting.texi, doc/ProofGeneral.texi: GPL, 3.4 dates * CHANGES, COPYING: GPL * FAQ: Isar is default over isa. * generic/span.el, generic/span-extent.el, generic/span-overlay.el, generic/texi-docstring-magic.el, generic/proof.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/proof-x-symbol.el, generic/proof-site.el, generic/proof-splash.el, generic/proof-syntax.el, generic/proof-shell.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-script.el, generic/pg-xhtml.el, generic/pg-xml.el, generic/proof-compat.el, generic/proof-config.el, generic/pg-metadata.el, generic/pg-pgip.el, generic/pg-user.el: GPL * BUGS: Mention looping GNU 2002-06-20 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html: Set version tag for new release. 2002-06-20 David Aspinall * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html: Set version tag for new release. 2002-06-19 Pierre Courtieu * CHANGES, doc/ProofGeneral.texi: Updated the doc and the CHANGES file about new backtracking for Coq. 2002-06-19 David Aspinall * generic/proof-menu.el: Match FSF C-button3 binding with XEmacs one * generic/proof-config.el: Doc improvements 2002-06-19 Pierre Courtieu * coq/coq-syntax.el: Finished updating the commands and tactic lists of coq-syntax.el. * coq/coq-syntax.el: updated the lists of commands and tactics in coq-syntax.el. 2002-06-19 David Aspinall * coq/coq.el: Use coq-proof-mode-p instead of nesting depth test. Attempt to track nesting depth (fails). * etc/coq/nested.v: Add nested section example to increase the horror. * etc/coq/nested.v: Added End for sections, and silly test * etc/debugging-tips.txt: Updated with more notes * coq/coq.el: Clean up: remove count-undos, comments, tweak coq-proof-mode-p. * ChangeLog: Updated. * generic/proof-shell.el: Add proof-shell-last-prompt. * doc/PG-adapting.texi: Add doc of proof-shell-last-prompt. * doc/ProofGeneral.texi: Fix info * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-06-18 David Aspinall * html/develdownload.php: Update Emacs versions * doc/ProofGeneral.texi: Add news for PG 3.4 * doc/PG-adapting.texi: Update magic. Document nested proof settings. * coq/coq.el: Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics. * generic/proof-script.el: Remove lift-global function. * generic/proof-config.el, generic/proof-script.el: Remove global testing and lift-global function; rename proof-nested-goals -> proof-nested-goals-history. * etc/coq/nested.v: Added some non-undoable tactics 2002-06-19 David Aspinall * generic/proof-shell.el: Add proof-shell-last-prompt. * doc/PG-adapting.texi: Add doc of proof-shell-last-prompt. * doc/ProofGeneral.texi: Fix info * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-06-18 David Aspinall * html/develdownload.php: Update Emacs versions * doc/ProofGeneral.texi: Add news for PG 3.4 * doc/PG-adapting.texi: Update magic. Document nested proof settings. * coq/coq.el: Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics. * generic/proof-script.el: Remove lift-global function. * generic/proof-config.el, generic/proof-script.el: Remove global testing and lift-global function; rename proof-nested-goals -> proof-nested-goals-history. * etc/coq/nested.v: Added some non-undoable tactics * etc/coq/nested.v: Added some sections * html/news.html, html/oldnews.html: News item for PG 3.4 2002-06-18 Pierre Courtieu * coq/coq.el, coq/coq-syntax.el: Added the backtrack mechanism for sections. Seems to work. * coq/coq.el, coq/coq-syntax.el: Added a function to inspect the prompt of Coq, in order to know if we are in proof-mode. Redundant with proof-nesting-depth. 2002-06-18 David Aspinall * coq/coq.el: Attempt at (alledgedly) more robust solution to find-and-forget. * etc/coq/nested.v: Fix * etc/coq/nested.v: Add more declarations * coq/coq.el: Test using proof-nesting-depth before calling Reset 2002-06-14 Pierre Courtieu * coq/coq.el: Minor changes. * coq/coq.el: Print and Check guess their argument from the region or the string near the point. 2002-06-13 David Aspinall * coq/coq.el: Disable count-undos function, just use find-and-forget. * generic/proof-script.el: A nil setting of proof-kill-goal-command forces use of proof-find-and-forget for all retraction. * generic/proof-config.el: Docs * generic/proof-shell.el: Experiment with showing real prover output for aborted proofs. 2002-06-12 David Aspinall * coq/coq.el: Revised find-and-forget function, which also works for count-undos. * etc/coq/nested.v: More test cases, summary of situation. * generic/span-overlay.el: Second variant of next-span, without doubly nested loop * generic/span-overlay.el: Improve imp of next-span * etc/coq/nested.v: Note of another bug * coq/coq.el: Test for find-and-forget using Back always instead of Reset. * etc/coq/nested.v: Add test t4 for extra depth of nesting * generic/proof-utils.el: Make hack for XEmacs 21.4 also work for later versions 2002-06-12 Pierre Courtieu * CHANGES: Changed the CHANGES file for Coq. * coq/coq.el: Nested proofs in Coq are well backtracked! I used the new field 'nestedundos created by David. Will change the CHANGE file accordingly. 2002-06-12 David Aspinall * generic/proof-script.el: Adjust proof-nesting depth, add FIXME notes since not right yet * isar/test.el: New files. * coq/coq.el: Add proof-nested-undo-regexp setting * generic/proof-script.el, generic/proof-config.el: Add nestedundos setting to span, and proof-nested-undo-regexp setting 2002-06-11 David Aspinall * etc/coq/nested.v: Replace with example from Pierre * generic/proof-script.el: Only match saves for prover that supports nested proofs (restores old behaviour for Isar). Isar goal/save regexps dont match up properly. 2002-06-11 Pierre Courtieu * CHANGES: Not important. * CHANGES: CHANGE is cleaner in the Coq part! Not important. * CHANGES: Added changes in CHANGE about my new customization variables coq-user-backable-command etc. * coq/coq.el, coq/coq-syntax.el: Added the coq-user-... elisp customization variables to allow the user to defclare new commands and tactics: must typically be customized in .emacs. 2002-06-11 David Aspinall * coq/coq.el: Remove proof-nested-goals-p setting * generic/proof-script.el: Improved proof-nesting-depth (not finished yet) 2002-06-11 Pierre Courtieu * coq/coq.el: Fixed a bug of the new synchro code (coq-find-and-forget) in coq.el. Now do not count Tactics and unsaved goal commands for "Back". 2002-06-11 David Aspinall * generic/proof-config.el, generic/proof-shell.el, generic/proof-script.el: Add proof-nesting-depth, new implementation of span amalgamation in proof-done-advancing. * coq/coq.el: Set nested goals; include Lemma again in def of goal. * etc/coq/nested.v: New files. 2002-06-08 David Aspinall * html/download.html: Mention not supporting E21 * ChangeLog: Updated. * etc/ProofGeneral.spec: Add install for isartags * ChangeLog: Updated. * isar/isar.el: Fix bug in string syntax in isar-strip-terminators: did this work correctly before? * generic/span.el: Clean up span.el loading; make compat with bbdb.el in FSF * generic/proof-shell.el: Clean up span.el loading * ChangeLog: Updated. * todo: Updates * acl2/example.acl2: Remove duplicate * etc/ProofGeneral.spec: Add isartags * isar/isartags: Program [broken] * doc/ProofGeneral.texi: Update magic * coq/coqtags, lego/legotags: Default to /usr/bin/perl * CHANGES: Note about removing dirs * html/projects.html: Remove PGK mention, other obs projects * ChangeLog: Updated. * generic/proof-script.el: Robustness fixes/bug notes * generic/proof-menu.el: Spacing * generic/span-extent.el: Tweak liveness test * generic/proof-site.el: Alter order * generic/proof-config.el: Fix keysym to use FSF syntax * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-06-08 David Aspinall * etc/ProofGeneral.spec: Add install for isartags * ChangeLog: Updated. * isar/isar.el: Fix bug in string syntax in isar-strip-terminators: did this work correctly before? * generic/span.el: Clean up span.el loading; make compat with bbdb.el in FSF * generic/proof-shell.el: Clean up span.el loading * ChangeLog: Updated. * todo: Updates * acl2/example.acl2: Remove duplicate * etc/ProofGeneral.spec: Add isartags * isar/isartags: Program [broken] * doc/ProofGeneral.texi: Update magic * coq/coqtags, lego/legotags: Default to /usr/bin/perl * CHANGES: Note about removing dirs * html/projects.html: Remove PGK mention, other obs projects * ChangeLog: Updated. * generic/proof-script.el: Robustness fixes/bug notes * generic/proof-menu.el: Spacing * generic/span-extent.el: Tweak liveness test * generic/proof-site.el: Alter order * generic/proof-config.el: Fix keysym to use FSF syntax * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-06-08 David Aspinall * isar/isar.el: Fix bug in string syntax in isar-strip-terminators: did this work correctly before? * generic/span.el: Clean up span.el loading; make compat with bbdb.el in FSF * generic/proof-shell.el: Clean up span.el loading * ChangeLog: Updated. * todo: Updates * acl2/example.acl2: Remove duplicate * etc/ProofGeneral.spec: Add isartags * isar/isartags: Program [broken] * doc/ProofGeneral.texi: Update magic * coq/coqtags, lego/legotags: Default to /usr/bin/perl * CHANGES: Note about removing dirs * html/projects.html: Remove PGK mention, other obs projects * ChangeLog: Updated. * generic/proof-script.el: Robustness fixes/bug notes * generic/proof-menu.el: Spacing * generic/span-extent.el: Tweak liveness test * generic/proof-site.el: Alter order * generic/proof-config.el: Fix keysym to use FSF syntax * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-06-08 David Aspinall * todo: Updates * acl2/example.acl2: Remove duplicate * etc/ProofGeneral.spec: Add isartags * isar/isartags: Program [broken] * doc/ProofGeneral.texi: Update magic * coq/coqtags, lego/legotags: Default to /usr/bin/perl * CHANGES: Note about removing dirs * html/projects.html: Remove PGK mention, other obs projects * ChangeLog: Updated. * generic/proof-script.el: Robustness fixes/bug notes * generic/proof-menu.el: Spacing * generic/span-extent.el: Tweak liveness test * generic/proof-site.el: Alter order * generic/proof-config.el: Fix keysym to use FSF syntax * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-06-08 David Aspinall * generic/proof-script.el: Robustness fixes/bug notes * generic/proof-menu.el: Spacing * generic/span-extent.el: Tweak liveness test * generic/proof-site.el: Alter order * generic/proof-config.el: Fix keysym to use FSF syntax * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-06-05 David Aspinall * isar/isar-keywords.el: Add types_code and friends 2002-05-29 Pierre Courtieu * coq/coq.el: Made a negative test to compute the number of "Back n" in coq-find-and-forget. * coq/coq.el, coq/coq-syntax.el: Modification of the coq-find-and-forget function, in order to use the new "Back n." command of coq to make the syncronization better. Seems to work, need to test. * coq/coq-syntax.el: Added some new tactic names 2002-05-21 David Aspinall * isa/isabelle-system.el: Mistake in function name (Norbert Voelker ) 2002-05-13 Markus Wenzel * doc/ProofGeneral.texi: updated URLxsymbol (unused); 2002-05-10 Markus Wenzel * isar/isar.el: tuned isar-strip-terminators; 2002-05-03 Markus Wenzel * TODO: fixed spelling; * isar/isar.el: tuned comment; * isar/todo, isar/isar.el: tuned proof-next-error setup; 2002-05-03 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * html/eproofe.php, html/eproofe: New files. * generic/proof-x-symbol.el: Fix X-symbol URL * generic/proof-utils.el: Fix font lock for E21 (I hope) * generic/proof-config.el: Try to support next-error key binding for both Emacs versions. * doc/ProofGeneral.texi: Reflect change in load order * CHANGES: Updates * generic/proof-site.el: Fix loading order to load Isar before Isa * isar/isar.el: Added support for proof-shell-next-error * isar/isar.el: Add support for proof-next-error. * generic/proof-config.el: Craftily set experimental fetures on for devel release. * generic/pg-user.el: Began adding generic line-width adjust 2002-05-03 David Aspinall * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * html/eproofe.php, html/eproofe: New files. * generic/proof-x-symbol.el: Fix X-symbol URL * generic/proof-utils.el: Fix font lock for E21 (I hope) * generic/proof-config.el: Try to support next-error key binding for both Emacs versions. * doc/ProofGeneral.texi: Reflect change in load order * CHANGES: Updates * generic/proof-site.el: Fix loading order to load Isar before Isa * isar/isar.el: Added support for proof-shell-next-error * isar/isar.el: Add support for proof-next-error. * generic/proof-config.el: Craftily set experimental fetures on for devel release. * generic/pg-user.el: Began adding generic line-width adjust 2002-04-24 David Aspinall * CHANGES: Remove indents * isa/isa-syntax.el: Updated list of SML keywords 2002-04-23 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html: Set version tag for new release. * doc/ProofGeneral.texi, doc/PG-adapting.texi, html/projects.html, html/screenshot.html, html/download.html, html/features.html, html/oldnews.html: Fix URL for X-symbol * todo: Updated * CHANGES: Add syntax highlighting cahanges from Lucas Dixon * isa/isa.el: Fix for E21 with isa-pre-shell-start. * isa/isa-syntax.el: Add syntax highlighting cahanges from Lucas Dixon 2002-04-23 David Aspinall * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html: Set version tag for new release. * doc/ProofGeneral.texi, doc/PG-adapting.texi, html/projects.html, html/screenshot.html, html/download.html, html/features.html, html/oldnews.html: Fix URL for X-symbol * todo: Updated * CHANGES: Add syntax highlighting cahanges from Lucas Dixon * isa/isa.el: Fix for E21 with isa-pre-shell-start. * isa/isa-syntax.el: Add syntax highlighting cahanges from Lucas Dixon 2002-03-22 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-03-22 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-03-22 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-03-21 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2002-03-21 David Aspinall * ChangeLog: Updated. * CHANGES: Improvement to ACL2 * acl2/acl2.el: Greatly improved support. * html/download.html: Typo * html/develdownload.php: No longer recommend XEmacs exclusively. * html/oldrel.php: FSF -> GNU * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Revert accidental commit by crr * CHANGES: Updated. * generic/proof.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/pg-pgip.el, generic/pg-user.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-splash.el, generic/pg-metadata.el: Year changes * generic/proof-shell.el: Remove toolbar gutters in multiple frame mode. Add proof-shell-truncate-before-error setting. * generic/proof-script.el: Dont set type property for proof elements (experiment). Tweak name determination/reporting. Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings * generic/proof-menu.el: Added activations for frame/window controls. * generic/proof-config.el: Added proof-shell-truncate-before-error, adjusted proof-toolbar-entries-default. * generic/proof-compat.el: Added emultation of display-graphic-p for XEmacs * generic/pg-xml.el: Add header to XML docs * generic/pg-xhtml.el: New files. * doc/PG-adapting.texi: Document some new settings 2002-03-21 Christophe Raffalli * phox/phox.el, phox/x-symbol-phox.el, generic/proof-config.el, generic/proof-utils.el, phox/phox-font.el, Makefile.devel: added hook: proof-before-fontify-output-hook 2002-03-21 David Aspinall * CHANGES: Improvement to ACL2 * acl2/acl2.el: Greatly improved support. * html/download.html: Typo * html/develdownload.php: No longer recommend XEmacs exclusively. * html/oldrel.php: FSF -> GNU * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Revert accidental commit by crr * CHANGES: Updated. * generic/proof.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/pg-pgip.el, generic/pg-user.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-splash.el, generic/pg-metadata.el: Year changes * generic/proof-shell.el: Remove toolbar gutters in multiple frame mode. Add proof-shell-truncate-before-error setting. * generic/proof-script.el: Dont set type property for proof elements (experiment). Tweak name determination/reporting. Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings * generic/proof-menu.el: Added activations for frame/window controls. * generic/proof-config.el: Added proof-shell-truncate-before-error, adjusted proof-toolbar-entries-default. * generic/proof-compat.el: Added emultation of display-graphic-p for XEmacs * generic/pg-xml.el: Add header to XML docs * generic/pg-xhtml.el: New files. * doc/PG-adapting.texi: Document some new settings 2002-03-21 Christophe Raffalli * phox/phox.el, phox/x-symbol-phox.el, generic/proof-config.el, generic/proof-utils.el, phox/phox-font.el, Makefile.devel: added hook: proof-before-fontify-output-hook 2002-03-21 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Revert accidental commit by crr * CHANGES: Updated. * generic/proof.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/pg-pgip.el, generic/pg-user.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-splash.el, generic/pg-metadata.el: Year changes * generic/proof-shell.el: Remove toolbar gutters in multiple frame mode. Add proof-shell-truncate-before-error setting. * generic/proof-script.el: Dont set type property for proof elements (experiment). Tweak name determination/reporting. Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings * generic/proof-menu.el: Added activations for frame/window controls. * generic/proof-config.el: Added proof-shell-truncate-before-error, adjusted proof-toolbar-entries-default. * generic/proof-compat.el: Added emultation of display-graphic-p for XEmacs * generic/pg-xml.el: Add header to XML docs * generic/pg-xhtml.el: New files. * doc/PG-adapting.texi: Document some new settings 2002-03-21 Christophe Raffalli * phox/phox.el, phox/x-symbol-phox.el, generic/proof-config.el, generic/proof-utils.el, phox/phox-font.el, Makefile.devel: added hook: proof-before-fontify-output-hook 2002-03-05 Christophe Raffalli * phox/phox.el, phox/phox-sym-lock.el, phox/README, phox/x-symbol-phox.el: *** empty log message *** 2002-02-23 David Aspinall * generic/proof-shell.el: Add check for Emacs21. * generic/pg-user.el: Bug fix in proof-goto-command-end. Decode x-syms in pg-insert-output-as-comment. * generic/proof-x-symbol.el: Simplify enabling tests to just check window-system. Fix proof-x-symbol-decode-region to return new END value after decoding. * generic/proof-utils.el: Updates to font-lock handling in proof-fontify-region, proof-font-lock-clear-font-lock-vars. Fix final return value in fontify region. * CHANGES: Update X-Sym status 2002-02-14 David Aspinall * Makefile.devel: Remove latest-src-rpm link * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-02-14 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-02-12 Markus Wenzel * isar/interface, isa/interface: option -g GEOMETRY; * isar/isar.el: observe isar-undo-ignore-regexp in isar-count-undos and isar-find-and-forget; * isar/isar-syntax.el: added isar-undo-ignore-regexp; 2002-02-08 Markus Wenzel * isar/isar.el: more robust proof-shell-interrupt-regexp and proof-shell-error-regexp; 2002-01-31 David Aspinall * ChangeLog: Updated. * html/about.html: Fix more broken front page links * INSTALL: Update for recent releases. * ChangeLog: Updated. * generic/proof-script.el: Simplify fix for repeated comments (commentre includes whitespace). * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-syntax.el: Tweak comment * generic/proof-script.el: Fix problem noticed with Isar and repeated comments. * etc/isar/CommentParsingBug.thy: New files. 2002-01-31 David Aspinall * html/about.html: Fix more broken front page links * INSTALL: Update for recent releases. * ChangeLog: Updated. * generic/proof-script.el: Simplify fix for repeated comments (commentre includes whitespace). * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-syntax.el: Tweak comment * generic/proof-script.el: Fix problem noticed with Isar and repeated comments. * etc/isar/CommentParsingBug.thy: New files. 2002-01-31 David Aspinall * generic/proof-script.el: Simplify fix for repeated comments (commentre includes whitespace). * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-syntax.el: Tweak comment * generic/proof-script.el: Fix problem noticed with Isar and repeated comments. * etc/isar/CommentParsingBug.thy: New files. 2002-01-31 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-syntax.el: Tweak comment * generic/proof-script.el: Fix problem noticed with Isar and repeated comments. * etc/isar/CommentParsingBug.thy: New files. 2002-01-26 Markus Wenzel * isar/isar-keywords.el: tuned comment; 2002-01-21 Markus Wenzel * isa/isabelle-system.el: full-proofs setting; * isa/README, isar/README: Isabelle2002 instead of Isabelle2001; 2002-01-17 Christophe Raffalli * phox/.cvsignore: *** empty log message *** 2002-01-16 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * lego/example.l, isar/Example.thy, coq/example.v: Whitespace * generic/proof.el: Comments * generic/proof-script.el: Also bury trace buffer * generic/proof-config.el: Comments * isa/Example.ML: Whitespace * generic/proof-shell.el: Only create trace buffer if liable to be used. Remove experimental spill-output style tracing code. * generic/proof-config.el, isar/isar.el, isa/isa.el: Set proof-shell-trace-output-regexp in proof-pre-shell-start-hook * isa/isa.el, isar/isar.el, generic/proof-config.el: Rename proof-shell-spill-output-regexp -> proof-shell-trace-output-regexp * doc/PG-adapting.texi: FSF Emacs -> GNU Emacs * doc/ProofGeneral.texi: Document the tracing buffer; FSF Emacs -> GNU Emacs 2002-01-16 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * lego/example.l, isar/Example.thy, coq/example.v: Whitespace * generic/proof.el: Comments * generic/proof-script.el: Also bury trace buffer * generic/proof-config.el: Comments * isa/Example.ML: Whitespace * generic/proof-shell.el: Only create trace buffer if liable to be used. Remove experimental spill-output style tracing code. * generic/proof-config.el, isar/isar.el, isa/isa.el: Set proof-shell-trace-output-regexp in proof-pre-shell-start-hook * isa/isa.el, isar/isar.el, generic/proof-config.el: Rename proof-shell-spill-output-regexp -> proof-shell-trace-output-regexp * doc/PG-adapting.texi: FSF Emacs -> GNU Emacs * doc/ProofGeneral.texi: Document the tracing buffer; FSF Emacs -> GNU Emacs 2002-01-15 David Aspinall * generic/proof-x-symbol.el: Also put trace buffer in x sym mode * ChangeLog: Updated. * generic/proof-shell.el: Remove defunct code * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/feedback.html: Deleted files. * CHANGES: Describe tracing improvements. * generic/proof-utils.el: windows-of-buffer -> get-buffer-window-list GNU name * generic/proof-shell.el: Inspect quit-flag when displaying tracing output; send an interrupt to the prover if set. * generic/proof-shell.el: Redisplay during tracing output on XEmacs * html/projects.html, html/download.html, html/gallery.php, html/links.html, html/main.html, html/oldnews.html: Fix link to feedback page 2002-01-15 David Aspinall * generic/proof-shell.el: Remove defunct code * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/feedback.html: Deleted files. * CHANGES: Describe tracing improvements. * generic/proof-utils.el: windows-of-buffer -> get-buffer-window-list GNU name * generic/proof-shell.el: Inspect quit-flag when displaying tracing output; send an interrupt to the prover if set. * generic/proof-shell.el: Redisplay during tracing output on XEmacs * html/projects.html, html/download.html, html/gallery.php, html/links.html, html/main.html, html/oldnews.html: Fix link to feedback page 2002-01-14 Markus Wenzel * etc/isar/trace_simp.thy: tuned; * etc/isar/trace_simp.thy: some test cases for trace_simp output; 2002-01-11 David Aspinall * COPYING: Fix numbering * CHANGES: Fix number * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2002-01-11 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-12-27 Markus Wenzel * isar/Example.thy: tuned; * isa/isabelle-system.el: trace_rules flag; * isar/BUGS, isa/README, isar/README, isar/todo: updated; * generic/README: fixed spelling; 2001-12-21 Markus Wenzel * isar/isar.el: do not set proof-shell-quit-cmd (admits persistent sessions); 2001-12-12 Markus Wenzel * isar/interface, isa/interface: incorporate smart X11 font installation (used to be in isatool installfonts); 2001-12-11 David Aspinall * ChangeLog: Updated. * html/develdownload.php, html/main.html: Be politically correct about FSF GNU Emacs; update to mention version 21. * html/news.html, html/oldnews.html: fix links to devel download. * ChangeLog: Updated. * html/news.html: News item about Emacs 21 support * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Note about Emacs 21 support and font lock. * generic/proof-utils.el: Protect XEmacs only code * generic/proof-site.el: Fix test for GNU 21 * generic/proof-script.el: Change to font-lock support routines. * generic/proof-menu.el: Disable customize-menu-create for Emacs 21. * generic/proof-utils.el: Rework font-lock variable munging to work in GNU Emacs 21 also. * generic/proof-shell.el: Missing paren * generic/proof-config.el: Remove double setting, leave test setting in. * generic/proof-shell.el: Simplify -goals-config-done and -response-config-done to use current buffer. Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames. * generic/proof-config.el: Added proof-trace-output-fontify-enable * CHANGES: Note of Emacs 21 support * generic/proof-toolbar.el: Add support for toolbars on Emacs 21. * generic/proof-splash.el: Add support for Emacs 21 image display. * generic/proof-site.el: Add proof-running-on-Emacs21 flag. * generic/proof-menu.el: Allow toolbar toggle for GNU Emacs 21. * html/features.html, generic/proof-config.el: Toolbar allowed in GNU Emacs 21 * generic/proof-compat.el: Add proof-emacs-imagep function for GNU Emacs 21. 2001-12-11 David Aspinall * html/develdownload.php, html/main.html: Be politically correct about FSF GNU Emacs; update to mention version 21. * html/news.html, html/oldnews.html: fix links to devel download. * ChangeLog: Updated. * html/news.html: News item about Emacs 21 support * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Note about Emacs 21 support and font lock. * generic/proof-utils.el: Protect XEmacs only code * generic/proof-site.el: Fix test for GNU 21 * generic/proof-script.el: Change to font-lock support routines. * generic/proof-menu.el: Disable customize-menu-create for Emacs 21. * generic/proof-utils.el: Rework font-lock variable munging to work in GNU Emacs 21 also. * generic/proof-shell.el: Missing paren * generic/proof-config.el: Remove double setting, leave test setting in. * generic/proof-shell.el: Simplify -goals-config-done and -response-config-done to use current buffer. Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames. * generic/proof-config.el: Added proof-trace-output-fontify-enable * CHANGES: Note of Emacs 21 support * generic/proof-toolbar.el: Add support for toolbars on Emacs 21. * generic/proof-splash.el: Add support for Emacs 21 image display. * generic/proof-site.el: Add proof-running-on-Emacs21 flag. * generic/proof-menu.el: Allow toolbar toggle for GNU Emacs 21. * html/features.html, generic/proof-config.el: Toolbar allowed in GNU Emacs 21 * generic/proof-compat.el: Add proof-emacs-imagep function for GNU Emacs 21. 2001-12-11 David Aspinall * html/news.html: News item about Emacs 21 support * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Note about Emacs 21 support and font lock. * generic/proof-utils.el: Protect XEmacs only code * generic/proof-site.el: Fix test for GNU 21 * generic/proof-script.el: Change to font-lock support routines. * generic/proof-menu.el: Disable customize-menu-create for Emacs 21. * generic/proof-utils.el: Rework font-lock variable munging to work in GNU Emacs 21 also. * generic/proof-shell.el: Missing paren * generic/proof-config.el: Remove double setting, leave test setting in. * generic/proof-shell.el: Simplify -goals-config-done and -response-config-done to use current buffer. Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames. * generic/proof-config.el: Added proof-trace-output-fontify-enable * CHANGES: Note of Emacs 21 support * generic/proof-toolbar.el: Add support for toolbars on Emacs 21. * generic/proof-splash.el: Add support for Emacs 21 image display. * generic/proof-site.el: Add proof-running-on-Emacs21 flag. * generic/proof-menu.el: Allow toolbar toggle for GNU Emacs 21. * html/features.html, generic/proof-config.el: Toolbar allowed in GNU Emacs 21 * generic/proof-compat.el: Add proof-emacs-imagep function for GNU Emacs 21. 2001-12-11 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Note about Emacs 21 support and font lock. * generic/proof-utils.el: Protect XEmacs only code * generic/proof-site.el: Fix test for GNU 21 * generic/proof-script.el: Change to font-lock support routines. * generic/proof-menu.el: Disable customize-menu-create for Emacs 21. * generic/proof-utils.el: Rework font-lock variable munging to work in GNU Emacs 21 also. * generic/proof-shell.el: Missing paren * generic/proof-config.el: Remove double setting, leave test setting in. * generic/proof-shell.el: Simplify -goals-config-done and -response-config-done to use current buffer. Kill trace buffer with other associated buffers, and set specifiers similarly for multiple frames. * generic/proof-config.el: Added proof-trace-output-fontify-enable * CHANGES: Note of Emacs 21 support * generic/proof-toolbar.el: Add support for toolbars on Emacs 21. * generic/proof-splash.el: Add support for Emacs 21 image display. * generic/proof-site.el: Add proof-running-on-Emacs21 flag. * generic/proof-menu.el: Allow toolbar toggle for GNU Emacs 21. * html/features.html, generic/proof-config.el: Toolbar allowed in GNU Emacs 21 * generic/proof-compat.el: Add proof-emacs-imagep function for GNU Emacs 21. 2001-12-10 David Aspinall * generic/proof-utils.el, generic/proof-shell.el: Add handling of proof-trace-buffer. * generic/proof.el: Added proof-trace-buffer. * generic/proof-utils.el, generic/proof-shell.el: Dont return a fontified string in proof-response-buffer-display. 2001-12-05 Markus Wenzel * generic/proof-shell.el: proof-release-lock: do not touch proof-shell-spill-output-buffer; proof-shell-spill-output-begin: reuse existing buffer; * isar/isar.el: activate proof-shell-spill-output-regexp; 2001-12-04 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Update for 3.4pre * html/devel.html: Update mailing list address (point to web page) 2001-12-04 Markus Wenzel * doc/PG-adapting.texi: update from make process; * doc/ProofGeneral.texi, isar/isar.el: isar specific commands for bold/sup/sub; * isa/x-symbol-isabelle.el: added symbols for alternative 0..9; 2001-12-04 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Update for 3.4pre * html/devel.html: Update mailing list address (point to web page) 2001-12-04 Markus Wenzel * doc/PG-adapting.texi: update from make process; * doc/ProofGeneral.texi, isar/isar.el: isar specific commands for bold/sup/sub; * isa/x-symbol-isabelle.el: added symbols for alternative 0..9; 2001-12-01 Markus Wenzel * isa/x-symbol-isabelle.el: \ symbol; use previously defined x-symbol-isabelle-user-table (or nil); x-symbol-user-table achieves electric |- and |= symbols; 2001-11-24 Markus Wenzel * isar/isar.el: proof-shell-spill-output-regexp temporarily disabled; 2001-11-20 Markus Wenzel * isar/isar.el: set proof-shell-spill-output-regexp; isar-activate-scripting: proof-syn-cd (why is this here needed?); 2001-11-13 Markus Wenzel * isa/interface, isar/interface: option -k for logic specific isar-keywords file; 2001-11-08 Markus Wenzel * isa/x-symbol-isabelle.el: added \ symbol; 2001-11-07 Markus Wenzel * isa/x-symbol-isabelle.el: added \ and \; * isar/isar-syntax.el: updated isar-goals-font-lock-keywords; 2001-10-24 David Aspinall * html/main.html: Fix missing arg to get. Add Paul Roziere as req'd by Christopphe Raffalli 2001-10-13 Markus Wenzel * isar/isar-syntax.el: isar-goals-font-lock-keywords: more general goal pattern; 2001-10-08 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Add back note. 2001-10-08 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * CHANGES: Add back note. 2001-10-04 Markus Wenzel * isar/isar.el: added isar-help-induct-rules; 2001-10-04 David Aspinall * CHANGES: Remove note for devel * generic/proof-toolbar.el: Fix fudged enabler to call button function interactively. 2001-09-26 Markus Wenzel * isa/x-symbol-isabelle.el: support \<^bold> control symbols; * generic/proof-config.el: fixed spelling; 2001-09-24 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * coq/coq.el: Add Lemma to exclusion for coq-goal-command-p. * doc/PG-adapting.texi: Update magic * doc/docstring-magic.el: New line * generic/proof-config.el: Fix error in docs of stop-silent-command, and name of pre-shell-start-hook. * doc/ProofGeneral.texi: Another bug reporter * generic/proof-shell.el: Implement Robert Schnecks idea to help Coq display whole of goals output. * CHANGES: Devel release is tweaked 3.3 2001-09-24 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * coq/coq.el: Add Lemma to exclusion for coq-goal-command-p. * doc/PG-adapting.texi: Update magic * doc/docstring-magic.el: New line * generic/proof-config.el: Fix error in docs of stop-silent-command, and name of pre-shell-start-hook. * doc/ProofGeneral.texi: Another bug reporter * generic/proof-shell.el: Implement Robert Schnecks idea to help Coq display whole of goals output. * CHANGES: Devel release is tweaked 3.3 2001-09-13 David Aspinall * ChangeLog: Updated. * doc/PG-adapting.texi: Link uref nicely * doc/ProofGeneral.texi: Minor improvements * doc/ProofGeneral.texi: Updates from an old printout of the manual * todo: updated * doc/PG-adapting.texi: Updates from an old printout of the manual * ChangeLog: Updated. * html/Kit/Makefile: New files. * html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd: Updated from Kit repo * html/download.html: Fix link * html/smallpage.php: Fix two more gaping holes letting people examine whole filesystem (also fixed in server anyway) * html/feedback, html/feedback.html, html/develdownload, html/develdownload.html, html/kit.php, html/kit, html/kit.html: PHP in php, html and no extn link to php * ChangeLog: Updated. * html/htmlshow.php: Fix two more gaping holes letting people examine whole filesystem * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/feedback: Feedback quick link * CHANGES: No changes msg * html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess: Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files 2001-09-13 David Aspinall * doc/PG-adapting.texi: Link uref nicely * doc/ProofGeneral.texi: Minor improvements * doc/ProofGeneral.texi: Updates from an old printout of the manual * todo: updated * doc/PG-adapting.texi: Updates from an old printout of the manual * ChangeLog: Updated. * html/Kit/Makefile: New files. * html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd: Updated from Kit repo * html/download.html: Fix link * html/smallpage.php: Fix two more gaping holes letting people examine whole filesystem (also fixed in server anyway) * html/feedback, html/feedback.html, html/develdownload, html/develdownload.html, html/kit.php, html/kit, html/kit.html: PHP in php, html and no extn link to php * ChangeLog: Updated. * html/htmlshow.php: Fix two more gaping holes letting people examine whole filesystem * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/feedback: Feedback quick link * CHANGES: No changes msg * html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess: Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files 2001-09-13 David Aspinall * html/Kit/Makefile: New files. * html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd: Updated from Kit repo * html/download.html: Fix link * html/smallpage.php: Fix two more gaping holes letting people examine whole filesystem (also fixed in server anyway) * html/feedback, html/feedback.html, html/develdownload, html/develdownload.html, html/kit.php, html/kit, html/kit.html: PHP in php, html and no extn link to php * ChangeLog: Updated. * html/htmlshow.php: Fix two more gaping holes letting people examine whole filesystem * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/feedback: Feedback quick link * CHANGES: No changes msg * html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess: Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files 2001-09-13 David Aspinall * html/htmlshow.php: Fix two more gaping holes letting people examine whole filesystem * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/feedback: Feedback quick link * CHANGES: No changes msg * html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess: Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files 2001-09-13 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/feedback: Feedback quick link * CHANGES: No changes msg * html/kit.html, html/mailinglist.html, html/develdownload.html, html/doc.html, html/feedback.html, html/kit, html/.htaccess: Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files 2001-09-10 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * etc/release-log.txt: Note about re-rel 3.3 * html/download.html, html/news.html: Update release dates * todo: Update todo * doc/ProofGeneral.texi: Remove spurious comment at start 2001-09-10 Markus Wenzel * isar/isar-syntax.el: isar-goals-font-lock-keywords: corollary; 2001-09-10 David Aspinall * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * etc/release-log.txt: Note about re-rel 3.3 * html/download.html, html/news.html: Update release dates * todo: Update todo * doc/ProofGeneral.texi: Remove spurious comment at start 2001-09-10 Markus Wenzel * isar/isar-syntax.el: isar-goals-font-lock-keywords: corollary; 2001-09-09 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * ChangeLog: Updated. * html/hits, html/hits.html: Renamed file * Makefile.devel: Fixup copying of releasename link * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Finished shift to 3.4 * html/kit: Link to kit.php * html/kit.html, html/kit.php: File determination nonsense * html/download.html: Change over to some .php files. * CHANGES: Backtrack to previous CHANGES file for now. * coq/README, lego/README: Coq/lego confusion * coq/BUGS: Bug in new parsing for coq, mention * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Update for 3.4pre * html/footer.html: Remove validation stamp from footer, since its a lie. * CHANGES: No changes yet * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-09 David Aspinall * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * ChangeLog: Updated. * html/hits, html/hits.html: Renamed file * Makefile.devel: Fixup copying of releasename link * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Finished shift to 3.4 * html/kit: Link to kit.php * html/kit.html, html/kit.php: File determination nonsense * html/download.html: Change over to some .php files. * CHANGES: Backtrack to previous CHANGES file for now. * coq/README, lego/README: Coq/lego confusion * coq/BUGS: Bug in new parsing for coq, mention * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Update for 3.4pre * html/footer.html: Remove validation stamp from footer, since its a lie. * CHANGES: No changes yet * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-09 David Aspinall * html/hits, html/hits.html: Renamed file * Makefile.devel: Fixup copying of releasename link * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Finished shift to 3.4 * html/kit: Link to kit.php * html/kit.html, html/kit.php: File determination nonsense * html/download.html: Change over to some .php files. * CHANGES: Backtrack to previous CHANGES file for now. * coq/README, lego/README: Coq/lego confusion * coq/BUGS: Bug in new parsing for coq, mention * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Update for 3.4pre * html/footer.html: Remove validation stamp from footer, since its a lie. * CHANGES: No changes yet * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-09 David Aspinall * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Finished shift to 3.4 * html/kit: Link to kit.php * html/kit.html, html/kit.php: File determination nonsense * html/download.html: Change over to some .php files. * CHANGES: Backtrack to previous CHANGES file for now. * coq/README, lego/README: Coq/lego confusion * coq/BUGS: Bug in new parsing for coq, mention * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Update for 3.4pre * html/footer.html: Remove validation stamp from footer, since its a lie. * CHANGES: No changes yet * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-09 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Update for 3.4pre * html/footer.html: Remove validation stamp from footer, since its a lie. * CHANGES: No changes yet * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-09 David Aspinall * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-06 Markus Wenzel * isa/interface, isar/interface: tuned usage; 2001-09-05 David Aspinall * doc/ProofGeneral.texi: Mention pg-toggle-visibility and its keybinding * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * generic/pg-metadata.el: Incomplete * doc/ProofGeneral.texi: Todo * CHANGES, todo: Updated * generic/proof-menu.el: Add keybindings for new commands for moving/navigating spans. * generic/proof-script.el: Fix problem with C-x C-v by copying buffer-file-name. Add children property to control spans. * generic/pg-user.el: Improved span moving and navigation commands. 2001-09-05 David Aspinall * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * generic/pg-metadata.el: Incomplete * doc/ProofGeneral.texi: Todo * CHANGES, todo: Updated * generic/proof-menu.el: Add keybindings for new commands for moving/navigating spans. * generic/proof-script.el: Fix problem with C-x C-v by copying buffer-file-name. Add children property to control spans. * generic/pg-user.el: Improved span moving and navigation commands. 2001-09-04 Markus Wenzel * isar/Example.thy: tuned proof text; added script version; * isa/interface, isar/interface: added option -P: actually start Proof General (default true); 2001-09-04 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/pg-xml.el: Issue parsing messages * generic/pg-user.el: Add commands to move spans up/down. Enable features only if experimental flag set * generic/proof-script.el: Nested proof spans are duplicable * generic/proof-config.el: Add experimental features setting * Makefile: Delete rogue elcs * CHANGES, INSTALL: Updates 2001-09-04 Markus Wenzel * isar/README: tuned; * isa/README, isar/README: no need to adjust the path to bash on the first line (due to /usr/bin/env); 2001-09-04 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/pg-xml.el: Issue parsing messages * generic/pg-user.el: Add commands to move spans up/down. Enable features only if experimental flag set * generic/proof-script.el: Nested proof spans are duplicable * generic/proof-config.el: Add experimental features setting * Makefile: Delete rogue elcs * CHANGES, INSTALL: Updates 2001-09-04 Markus Wenzel * isar/README: tuned; * isa/README, isar/README: no need to adjust the path to bash on the first line (due to /usr/bin/env); 2001-09-03 David Aspinall * ChangeLog: Updated. * README.devel: Text * ChangeLog: Trim dups * README.windows: Add author * TODO, CHANGES: Updated * isa/Example.ML: Accidental commit; revert to original. * isar/isar.el: Set proof-goal-with-hole-regexp * generic/proof-config.el: Change colour of locked region. * generic/proof-shell.el: Fix bracket bug. * generic/proof-script.el: Show/hide all proofs: add redisplay for FSF Use new functions pg-set-span-helphighlights and pg-span-name to set help echo, balloon help, mouse highlight, and context menu. * generic/proof-depends.el: Use pg-set-span-helphightlights for unhighlighting. * generic/pg-user.el: Generalise context menu for other spans; grey out show/hide when unavailable. * html/main.html: Join paras * ChangeLog: Updated. * html/features.html: Text * html/features.html: Fix link to screenshot * html/doc.html: Improve layout * doc/PG-adapting.texi, doc/ProofGeneral.texi: Update version numbers, time stamps. * html/download.html: Typo. Update Emacs version to 20.7. * ChangeLog: Updated. * html/oldrel.php: Update branch * html/download.html: PHP file * html/oldrel.html, html/oldrel.php: Renamed file * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/download.html: Please try devel version * bin/proofgeneral, demoisa/demoisa.el: Accidental update; revert to previous * demoisa/README: Rearrange * twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/twelf-old.el, plastic/todo, twelf/example.elf, twelf/README, twelf/twelf-font.el, plastic/plastic.el, plastic/plastic-syntax.el, plastic/test.lf, phox/phox.el, plastic/README, phox/phox-outline.el, phox/phox-sym-lock.el, phox/phox-tags.el, phox/example.phx, phox/phox-extraction.el, phox/phox-font.el, phox/phox-fun.el, lego/readonly/readonly.l, papers/README, phox/README, lego/legotags, lego/todo, lego/x-symbol-lego.el, lego/example2.l, lego/lego.el, lego/lego-syntax.el, lego/BUGS, lego/example.l, lego/README, isar/todo, isar/isar.el, isar/isar-keywords.el, isar/isar-syntax.el, isar/BUGS, isar/Example.thy, isar/interface, isar/README, isa/todo, isa/x-symbol-isabelle.el, isa/isabelle-system.el, isa/thy-mode.el, isa/isa.el, isa/interface, isa/interface-setup.el, isa/isa-syntax.el, isa/depends.ML, isa/Example2.ML, isa/README, isa/BUGS, isa/Example.ML, isa/Example.thy, isa/Example-Xsym.ML, images/gimp/.cvsignore, images/gimp/scripts/proofgeneral.scm, images/use.8bit.xpm, images/use.xcf, images/use.xpm, images/undo.8bit.xpm, images/undo.xcf, images/undo.xpm, images/retract.xpm, images/state.8bit.xpm, images/state.xcf, images/state.xpm, images/restart.xpm, images/retract.8bit.xpm, images/retract.xcf, images/qed.xpm, images/restart.8bit.xpm, images/restart.xcf, images/pgicon.png, images/pgmini.xpm, images/qed.8bit.xpm, images/qed.xcf, images/pg-text.xcf, images/pg-text.8bit.gif, images/pg-text.gif, images/pg-text.jpg, images/next.xcf, images/next.xpm, images/notes.txt, images/next.8bit.xpm, images/lego-badge.xcf, images/isabelle_transparent.8bit.gif, images/isabelle_transparent.gif, images/isabelle_transparent.xcf, images/isabelle-badge.xcf, images/info.xpm, images/interrupt.8bit.xpm, images/interrupt.xcf, images/interrupt.xpm, images/help.xpm, images/info.8bit.xpm, images/info.xcf, images/goto.xcf, images/goto.xpm, images/help.8bit.xpm, images/help.xcf, images/goto.8bit.xpm, images/goal_large.xcf, images/goal.8bit.xpm, images/goal.xcf, images/goal.xpm, images/find.xpm, images/fireworks.xcf, images/find.8bit.xpm, images/find.xcf, images/context.xpm, images/coq-badge.xcf, images/command.xcf, images/command.xpm, images/context.8bit.xpm, images/context.xcf, images/abort.xpm, images/blank.xcf, images/command.8bit.xpm, images/abort.8bit.xpm, images/abort.xcf, images/README, images/ProofGeneral.jpg, images/ProofGeneral.xcf, images/ProofGeneral.8bit.gif, images/ProofGeneral.gif, images/.cvsignore, images/Makefile, html/projects/test.html, html/projects/thybrowse.html, html/projects/webreplay.html, html/projects/xmlpgip.html, html/projects/pgip.html, html/projects/pgml.html, html/projects/reelcase.html, html/projects/scrgen.html, html/projects/hol.html, html/projects/isapbp.html, html/projects/mm.html, html/projects/outline.html, html/projects/coqfile.html, html/projects/coqpbp.html, html/projects/corba.html, html/projects/acs.html, html/papers/pgtalk.pdf, html/papers/pgoutline.ps.gz, html/papers/pgoutline.pdf, html/images/whole-man.jpg, html/images/whole-man-thumb.jpg, html/images/silverrule.gif, html/images/vh40.gif, html/images/whip.jpg, html/images/whip-thumb.jpg, html/images/pg-text.gif, html/images/portrait.jpg, html/images/portrait-thumb.jpg, html/images/pg-lego-console.png, html/images/pg-lego-screenshot.png, html/images/pg-lego-thumb.png, html/images/pg-isar-thumb.png, html/images/pg-lego-console-thumb.png, html/images/pg-isar-screenshot.png, html/images/pg-isa-screenshot.png, html/images/pg-isa-thumb.png, html/images/pg-coq-thumb.png, html/images/isabelle.gif, html/images/lego-badge.gif, html/images/pg-coq-screenshot.png, html/images/canvaswallpaper.jpg, html/images/coq-badge.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf, html/images/isabelle-badge.gif, html/images/bullethole.gif, html/images/PG-small.jpg, html/images/ProofGeneral.jpg, html/images/.cvsignore, html/images/IsaPGscreen.jpg, .cvsignore, html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd, html/smallpage.php, html/screenshot.html, html/smallheader.html, html/smallpage.html, html/proofgen.css, html/register, html/register.html, html/screenshot, html/oldnews.html, html/oldrel.html, html/projects.html, html/news, html/news.html, html/notes.txt, html/main, html/main.html, html/mission.html, html/links, html/links.html, html/mailinglist, html/mailinglist.html, html/index.php, html/index.shtml, html/kit, html/kit.html, html/htmlshow.html, html/htmlshow.php, html/gallery.php, html/header.html, html/head.html, html/hits.html, html/fileshow.php, html/footer.html, html/functions.php3, html/gallery, html/features.html, html/feedback.html, html/feedback.php, html/download, html/download.html, html/elispmarkup.php3, html/features, html/develdownload.php, html/doc, html/doc.html, html/develdownload.html, html/cvsweb.conf, html/devel, html/devel.html, html/counter.php3, html/cvsweb.cgi, html/about, html/about.html, html/.cvsignore, html/ProofGeneralPortrait.eps.gz, hol98/example.sml, hol98/hol98.el, hol98/todo, hol98/x-symbol-hol98.el, generic/span.el, generic/texi-docstring-magic.el, hol98/README, generic/span-extent.el, generic/span-overlay.el, generic/proof.el, generic/proof-x-symbol.el, generic/proof-utils.el, generic/proof-syntax.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-splash.el, generic/proof-site.el, generic/proof-shell.el, generic/proof-script.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, etc/pgkit/xmltest1.xml, etc/pgkit/xmltest2.xml, generic/_pkg.el, generic/README, etc/patches/duplicated-short-messages-fix.txt, etc/patches/fix-attempt-for-eager-cleaning.txt, etc/lego/multiple/C.l, etc/lego/multiple/D.l, etc/lego/multiple/README, etc/lego/multiple/A.l, etc/lego/multiple/B.l, etc/lego/unsaved-goals.l, etc/lego/error-eg.l, etc/lego/lego-site.el, etc/lego/long-line-backslash.l, etc/isar/multiple/README, etc/lego/GoalGoal.l, etc/isar/multiple/A.thy, etc/isar/multiple/B.thy, etc/isar/multiple/C.thy, etc/isar/multiple/D.thy, etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README, etc/isar/XEmacsSyntacticContextProb.thy, etc/demoisa/README, etc/isar/Parsing.thy, etc/demoisa/A.ML, etc/demoisa/B.ML, etc/demoisa/C.ML, etc/demoisa/D.ML, etc/isa/multiple/foobar/foo.ML, etc/isa/thy/test.ML, etc/isa/multiple/D.thy, etc/isa/multiple/Err.ML, etc/isa/multiple/Err.thy, etc/isa/multiple/README, etc/isa/multiple/B.thy, etc/isa/multiple/C.ML, etc/isa/multiple/C.thy, etc/isa/multiple/D.ML, etc/isa/multiple/A.ML, etc/isa/multiple/A.thy, etc/isa/multiple/B.ML, etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/\backslashname/test.ML, etc/isa/\backslashname/test.thy, etc/isa/long-line-backslash.ML, etc/isa/message-test.ML, etc/isa/settings.ML, etc/isa/xsym.ML, etc/coq/multiple/c.v, etc/isa/goal-matching.ML, etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/.cvsignore, etc/coq/multiple/README, etc/coq/unnamed_thm.v, etc/testing-log.txt, etc/proofgeneral-domain.txt, etc/release-log.txt, etc/screenshot-notes.txt, etc/test-schedule.txt, etc/doc-notes.txt, etc/junk.el, etc/profiling.txt, etc/bug-notes.txt, etc/cvs-tips.txt, etc/debugging-tips.txt, etc/announce, etc/README, etc/TESTS, etc/ProofGeneral.menu, etc/ProofGeneral.spec, doc/dir, doc/docstring-magic.el, doc/localdir, doc/README.doc, doc/ProofGeneral.jpg, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile, demoisa/demoisa-easy.el, demoisa/demoisa.el, coq/todo, coq/x-symbol-coq.el, demoisa/README, coq/coqtags, coq/example.v, coq/coq.el, coq/BUGS, coq/coq-syntax.el, coq/README, acl2/example.acl2, acl2/x-symbol-acl2.el, bin/proofgeneral, acl2/acl2.el, acl2/README, todo, README.devel, README.windows, REGISTER, TODO, Makefile.xemacs, README, Makefile, Makefile.devel, FAQ, INSTALL, ChangeLog, COPYING, BUGS, CHANGES, AUTHORS: Updating branch * doc/ProofGeneral.texi: Note of what to do * generic/proof-script.el: Formatting * html/features.html: Mention hiding proofs. * etc/ProofGeneral.spec: Add specific READMEs. * etc/cvs-tips.txt: Note of secure alt to no password * etc/release-log.txt: Ready for release * etc/announce: Update for 3.3 * plastic/README, twelf/README, isa/README, isar/README, lego/README, phox/README, hol98/README, coq/README, generic/README, acl2/README: Add specific install instrs, rearrange. * INSTALL: Move specific install instructions into subdirs * isa/isa.el: Add settings for testing trace buffers. * CHANGES: Note about tracing buffers for developers * generic/proof-shell.el: Added handling of tracing buffers using proof-shell-spill-output-regexp. * generic/proof-config.el: Added proof-shell-spill-output-regexp 2001-09-03 David Aspinall * README.devel: Text * ChangeLog: Trim dups * README.windows: Add author * TODO, CHANGES: Updated * isa/Example.ML: Accidental commit; revert to original. * isar/isar.el: Set proof-goal-with-hole-regexp * generic/proof-config.el: Change colour of locked region. * generic/proof-shell.el: Fix bracket bug. * generic/proof-script.el: Show/hide all proofs: add redisplay for FSF Use new functions pg-set-span-helphighlights and pg-span-name to set help echo, balloon help, mouse highlight, and context menu. * generic/proof-depends.el: Use pg-set-span-helphightlights for unhighlighting. * generic/pg-user.el: Generalise context menu for other spans; grey out show/hide when unavailable. * html/main.html: Join paras * ChangeLog: Updated. * html/features.html: Text * html/features.html: Fix link to screenshot * html/doc.html: Improve layout * doc/PG-adapting.texi, doc/ProofGeneral.texi: Update version numbers, time stamps. * html/download.html: Typo. Update Emacs version to 20.7. * ChangeLog: Updated. * html/oldrel.php: Update branch * html/download.html: PHP file * html/oldrel.html, html/oldrel.php: Renamed file * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/download.html: Please try devel version * bin/proofgeneral, demoisa/demoisa.el: Accidental update; revert to previous * demoisa/README: Rearrange * twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/twelf-old.el, plastic/todo, twelf/example.elf, twelf/README, twelf/twelf-font.el, plastic/plastic.el, plastic/plastic-syntax.el, plastic/test.lf, phox/phox.el, plastic/README, phox/phox-outline.el, phox/phox-sym-lock.el, phox/phox-tags.el, phox/example.phx, phox/phox-extraction.el, phox/phox-font.el, phox/phox-fun.el, lego/readonly/readonly.l, papers/README, phox/README, lego/legotags, lego/todo, lego/x-symbol-lego.el, lego/example2.l, lego/lego.el, lego/lego-syntax.el, lego/BUGS, lego/example.l, lego/README, isar/todo, isar/isar.el, isar/isar-keywords.el, isar/isar-syntax.el, isar/BUGS, isar/Example.thy, isar/interface, isar/README, isa/todo, isa/x-symbol-isabelle.el, isa/isabelle-system.el, isa/thy-mode.el, isa/isa.el, isa/interface, isa/interface-setup.el, isa/isa-syntax.el, isa/depends.ML, isa/Example2.ML, isa/README, isa/BUGS, isa/Example.ML, isa/Example.thy, isa/Example-Xsym.ML, images/gimp/.cvsignore, images/gimp/scripts/proofgeneral.scm, images/use.8bit.xpm, images/use.xcf, images/use.xpm, images/undo.8bit.xpm, images/undo.xcf, images/undo.xpm, images/retract.xpm, images/state.8bit.xpm, images/state.xcf, images/state.xpm, images/restart.xpm, images/retract.8bit.xpm, images/retract.xcf, images/qed.xpm, images/restart.8bit.xpm, images/restart.xcf, images/pgicon.png, images/pgmini.xpm, images/qed.8bit.xpm, images/qed.xcf, images/pg-text.xcf, images/pg-text.8bit.gif, images/pg-text.gif, images/pg-text.jpg, images/next.xcf, images/next.xpm, images/notes.txt, images/next.8bit.xpm, images/lego-badge.xcf, images/isabelle_transparent.8bit.gif, images/isabelle_transparent.gif, images/isabelle_transparent.xcf, images/isabelle-badge.xcf, images/info.xpm, images/interrupt.8bit.xpm, images/interrupt.xcf, images/interrupt.xpm, images/help.xpm, images/info.8bit.xpm, images/info.xcf, images/goto.xcf, images/goto.xpm, images/help.8bit.xpm, images/help.xcf, images/goto.8bit.xpm, images/goal_large.xcf, images/goal.8bit.xpm, images/goal.xcf, images/goal.xpm, images/find.xpm, images/fireworks.xcf, images/find.8bit.xpm, images/find.xcf, images/context.xpm, images/coq-badge.xcf, images/command.xcf, images/command.xpm, images/context.8bit.xpm, images/context.xcf, images/abort.xpm, images/blank.xcf, images/command.8bit.xpm, images/abort.8bit.xpm, images/abort.xcf, images/README, images/ProofGeneral.jpg, images/ProofGeneral.xcf, images/ProofGeneral.8bit.gif, images/ProofGeneral.gif, images/.cvsignore, images/Makefile, html/projects/test.html, html/projects/thybrowse.html, html/projects/webreplay.html, html/projects/xmlpgip.html, html/projects/pgip.html, html/projects/pgml.html, html/projects/reelcase.html, html/projects/scrgen.html, html/projects/hol.html, html/projects/isapbp.html, html/projects/mm.html, html/projects/outline.html, html/projects/coqfile.html, html/projects/coqpbp.html, html/projects/corba.html, html/projects/acs.html, html/papers/pgtalk.pdf, html/papers/pgoutline.ps.gz, html/papers/pgoutline.pdf, html/images/whole-man.jpg, html/images/whole-man-thumb.jpg, html/images/silverrule.gif, html/images/vh40.gif, html/images/whip.jpg, html/images/whip-thumb.jpg, html/images/pg-text.gif, html/images/portrait.jpg, html/images/portrait-thumb.jpg, html/images/pg-lego-console.png, html/images/pg-lego-screenshot.png, html/images/pg-lego-thumb.png, html/images/pg-isar-thumb.png, html/images/pg-lego-console-thumb.png, html/images/pg-isar-screenshot.png, html/images/pg-isa-screenshot.png, html/images/pg-isa-thumb.png, html/images/pg-coq-thumb.png, html/images/isabelle.gif, html/images/lego-badge.gif, html/images/pg-coq-screenshot.png, html/images/canvaswallpaper.jpg, html/images/coq-badge.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf, html/images/isabelle-badge.gif, html/images/bullethole.gif, html/images/PG-small.jpg, html/images/ProofGeneral.jpg, html/images/.cvsignore, html/images/IsaPGscreen.jpg, .cvsignore, html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd, html/smallpage.php, html/screenshot.html, html/smallheader.html, html/smallpage.html, html/proofgen.css, html/register, html/register.html, html/screenshot, html/oldnews.html, html/oldrel.html, html/projects.html, html/news, html/news.html, html/notes.txt, html/main, html/main.html, html/mission.html, html/links, html/links.html, html/mailinglist, html/mailinglist.html, html/index.php, html/index.shtml, html/kit, html/kit.html, html/htmlshow.html, html/htmlshow.php, html/gallery.php, html/header.html, html/head.html, html/hits.html, html/fileshow.php, html/footer.html, html/functions.php3, html/gallery, html/features.html, html/feedback.html, html/feedback.php, html/download, html/download.html, html/elispmarkup.php3, html/features, html/develdownload.php, html/doc, html/doc.html, html/develdownload.html, html/cvsweb.conf, html/devel, html/devel.html, html/counter.php3, html/cvsweb.cgi, html/about, html/about.html, html/.cvsignore, html/ProofGeneralPortrait.eps.gz, hol98/example.sml, hol98/hol98.el, hol98/todo, hol98/x-symbol-hol98.el, generic/span.el, generic/texi-docstring-magic.el, hol98/README, generic/span-extent.el, generic/span-overlay.el, generic/proof.el, generic/proof-x-symbol.el, generic/proof-utils.el, generic/proof-syntax.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-splash.el, generic/proof-site.el, generic/proof-shell.el, generic/proof-script.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, etc/pgkit/xmltest1.xml, etc/pgkit/xmltest2.xml, generic/_pkg.el, generic/README, etc/patches/duplicated-short-messages-fix.txt, etc/patches/fix-attempt-for-eager-cleaning.txt, etc/lego/multiple/C.l, etc/lego/multiple/D.l, etc/lego/multiple/README, etc/lego/multiple/A.l, etc/lego/multiple/B.l, etc/lego/unsaved-goals.l, etc/lego/error-eg.l, etc/lego/lego-site.el, etc/lego/long-line-backslash.l, etc/isar/multiple/README, etc/lego/GoalGoal.l, etc/isar/multiple/A.thy, etc/isar/multiple/B.thy, etc/isar/multiple/C.thy, etc/isar/multiple/D.thy, etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README, etc/isar/XEmacsSyntacticContextProb.thy, etc/demoisa/README, etc/isar/Parsing.thy, etc/demoisa/A.ML, etc/demoisa/B.ML, etc/demoisa/C.ML, etc/demoisa/D.ML, etc/isa/multiple/foobar/foo.ML, etc/isa/thy/test.ML, etc/isa/multiple/D.thy, etc/isa/multiple/Err.ML, etc/isa/multiple/Err.thy, etc/isa/multiple/README, etc/isa/multiple/B.thy, etc/isa/multiple/C.ML, etc/isa/multiple/C.thy, etc/isa/multiple/D.ML, etc/isa/multiple/A.ML, etc/isa/multiple/A.thy, etc/isa/multiple/B.ML, etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/\backslashname/test.ML, etc/isa/\backslashname/test.thy, etc/isa/long-line-backslash.ML, etc/isa/message-test.ML, etc/isa/settings.ML, etc/isa/xsym.ML, etc/coq/multiple/c.v, etc/isa/goal-matching.ML, etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/.cvsignore, etc/coq/multiple/README, etc/coq/unnamed_thm.v, etc/testing-log.txt, etc/proofgeneral-domain.txt, etc/release-log.txt, etc/screenshot-notes.txt, etc/test-schedule.txt, etc/doc-notes.txt, etc/junk.el, etc/profiling.txt, etc/bug-notes.txt, etc/cvs-tips.txt, etc/debugging-tips.txt, etc/announce, etc/README, etc/TESTS, etc/ProofGeneral.menu, etc/ProofGeneral.spec, doc/dir, doc/docstring-magic.el, doc/localdir, doc/README.doc, doc/ProofGeneral.jpg, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile, demoisa/demoisa-easy.el, demoisa/demoisa.el, coq/todo, coq/x-symbol-coq.el, demoisa/README, coq/coqtags, coq/example.v, coq/coq.el, coq/BUGS, coq/coq-syntax.el, coq/README, acl2/example.acl2, acl2/x-symbol-acl2.el, bin/proofgeneral, acl2/acl2.el, acl2/README, todo, README.devel, README.windows, REGISTER, TODO, Makefile.xemacs, README, Makefile, Makefile.devel, FAQ, INSTALL, ChangeLog, COPYING, BUGS, CHANGES, AUTHORS: Updating branch * doc/ProofGeneral.texi: Note of what to do * generic/proof-script.el: Formatting * html/features.html: Mention hiding proofs. * etc/ProofGeneral.spec: Add specific READMEs. * etc/cvs-tips.txt: Note of secure alt to no password * etc/release-log.txt: Ready for release * etc/announce: Update for 3.3 * plastic/README, twelf/README, isa/README, isar/README, lego/README, phox/README, hol98/README, coq/README, generic/README, acl2/README: Add specific install instrs, rearrange. * INSTALL: Move specific install instructions into subdirs * isa/isa.el: Add settings for testing trace buffers. * CHANGES: Note about tracing buffers for developers * generic/proof-shell.el: Added handling of tracing buffers using proof-shell-spill-output-regexp. * generic/proof-config.el: Added proof-shell-spill-output-regexp 2001-09-02 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-09-02 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-08-31 Markus Wenzel * isa/interface, isar/interface: handle relative heap paths gracefully; * isar/isar-keywords.el: back to *official* Isabelle99-2 (later Isabelle dists will provide their own copy of this file); 2001-08-31 David Aspinall * CHANGES: Improved explanation * doc/ProofGeneral.texi: Something about dependencies feature * CHANGES: Added note about dependency feature. * generic/proof-depends.el: (Almost) complete rewrite * generic/proof-autoloads.el: Updated * generic/proof-script.el: Move theorem dependency code into proof-depends.el. Added 'controlspan property to proof body spans: action will be controlled from the control span. (The 'goalsave is the parent). Replace 'highlight face with 'proof-mouse-highlight-face throughout. * generic/pg-user.el: Added copy command, call to dependency menu if proof-depends is loaded. * isa/depends.ML: Add simulations of more qed commands, also sort and uniquify dependencies. * generic/proof-config.el: Add new proof-mouse-highlight-face to use instead of default. Fix dependency faces. 2001-08-31 Markus Wenzel * isar/isar-keywords.el: new commands (proof terms, code generator); 2001-08-31 David Aspinall * ChangeLog: Remove duplicate entries * generic/proof-config.el: Add faces for theorem dependencies. * etc/coq/multiple/README: Explanation * AUTHORS: Add DvO to list * AUTHORS: Add Christophe to list * coq/coq.el: Add auto-compile-vos experimental setting for automatic multiple files. * BUGS: Remove minibuffer bug * isa/thy-mode.el: Fix for names of functions in proof-depends * isa/isa.el: Add setting for turning on theorem dependency tracking * isa/depends.ML: Update for Isabelle99-2 * generic/proof-depends.el, generic/proof-script.el: Clean up of proof-depends * generic/proof-menu.el: Skip settings which have no PA command in proof-assistant-settings-cmd * generic/proof-shell.el: Add proof-shell-kill-function-hooks 2001-08-30 Markus Wenzel * isa/interface, isar/interface: include ISABELLE_HOME_USER/etc/isar-keywords.el or ISABELLE_HOME/etc/isar-keywords.el if available; * isa/README, isar/README, isar/todo: updated; * generic/proof-script.el: pg-add-proof-element: removed accidential (?) dynamic scoping on proofbodyspan; handle proof-script-integral-proofs; * generic/proof-config.el: added proof-script-integral-proofs ("Whether the complete text after a goal confines the actual proof."); * isar/isar.el: proof-script-integral-proofs t; 2001-08-30 David Aspinall * ChangeLog: Updated. * CHANGES: Clarify 6.3.1 for multi file * isa/isabelle-system.el: Fix interrupt hook for PolyML 4 in recent Isabelle * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-shell.el: Add reassurance to interrupt warning to make Markus happier. * html/download.html: Note about XEmacs 21 and x-symbol * isa/isabelle-system.el: Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3). * CHANGES: More about invisible proofs and multiple files in Coq. X-symbol compat * generic/proof-x-symbol.el: Updates for recent version of X-symbol, which has no file called x-symbol-autoloads. * generic/proof-menu.el: Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings. * generic/proof.el: Add variable proof-previous-script-buffer * generic/proof-script.el: fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated * generic/proof-compat.el: Added implementation of remassq for FSF Emacs * generic/pg-user.el: pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment. 2001-08-30 David Aspinall * CHANGES: Clarify 6.3.1 for multi file * isa/isabelle-system.el: Fix interrupt hook for PolyML 4 in recent Isabelle * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-shell.el: Add reassurance to interrupt warning to make Markus happier. * html/download.html: Note about XEmacs 21 and x-symbol * isa/isabelle-system.el: Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3). * CHANGES: More about invisible proofs and multiple files in Coq. X-symbol compat * generic/proof-x-symbol.el: Updates for recent version of X-symbol, which has no file called x-symbol-autoloads. * generic/proof-menu.el: Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings. * generic/proof.el: Add variable proof-previous-script-buffer * generic/proof-script.el: fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated * generic/proof-compat.el: Added implementation of remassq for FSF Emacs * generic/pg-user.el: pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment. 2001-08-28 David Aspinall * doc/PG-adapting.texi, doc/ProofGeneral.texi: Fix web page for kit 2001-08-28 Pierre Courtieu * doc/ProofGeneral.texi: added something in the doc about coq-version-is-V7. * coq/coq.el: Added something in the doc about coq-version-is-V7, and made the setting of this variable more trustable with (concat coq-prog-name "-v"). 2001-08-28 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-script.el: Change of proof span type back to goalsave fix * lego/lego.el, coq/coq.el, phox/phox-fun.el, isar/isar.el: Change of proof span type back to goalsave * generic/proof-splash.el: Remove dependent setting of timeout, since bin calls different fn now. * bin/proofgeneral: Call function which always waits to prevent odd mode selection bug. * generic/proof-splash.el: Trivial * generic/proof-splash.el: Remove mention of toolbar variable. Make timeouts vary according to how started. * generic/proof-splash.el: Timeout happens as intended now, while loading some parts of PG. * html/header.html, html/proofgen.css: Improve stylesheet syntax, make menubar smaller 2001-08-17 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-script.el: Trim visibility implementation: - remove visibility specs and script portion records during undo - clear visibility specs on restart * generic/span-extent.el, generic/span-overlay.el: Add span-delete-action hook * CHANGES: Minibuffer contents bug fix * generic/proof-utils.el: Fix bug in proof-display-and-keep-buffer which had resulted in switching minibuffer windows buffer. 2001-08-16 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * doc/ProofGeneral.texi: Document visibility control * html/devel.html: Add link to browse files * html/download.html: Add link to browse package * html/develdownload.php: Add link to individual files * CHANGES: Move visibility item up, removed "in progress" * generic/proof-shell.el: Switch back to using goalsave spans in PBP code * generic/proof-config.el, generic/proof-toolbar.el: Add hide/show commands instead of make proofs visible * generic/proof-script.el: Generate intermediate proof span for contents of proof; other becomes 'goalsave again. Add idiom property. * generic/pg-user.el: Function name fixes, use idiom property in span for popup menu name. 2001-08-15 David Aspinall * html/gallery.php: Fix screenshots link * html/gallery: Fix again. * html/gallery: Fix link 2001-08-10 David Aspinall * ChangeLog: Updated. * CHANGES: Explain symptom properly * generic/proof-script.el: Use proof-looking-at-syntactic-context function from proof-syntax, as suggested by Markus * generic/proof-syntax.el: Found another instance of buffer-syntactic-context * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Put all in dist except pgkit * README: Rearrange list of assistants, note REGISTER. * FAQ: Remove note about 3.1 * BUGS: Comment about win32 XEmacs * generic/proof-compat.el: Workaround for buffer-syntactic-context bug in XEmacs 21.1 * generic/proof-script.el, isar/isar.el: Change buffer-syntactic-context -> proof-buffer-syntactic-context * etc/isar/XEmacsSyntacticContextProb.thy: Bug test case, note workaround date * etc/isar/XEmacsSyntacticContextProb.thy: Bug test case * CHANGES: Note of bug fix for buffer-syntactic-context 2001-08-09 Markus Wenzel * isa/x-symbol-isabelle.el: fixed potential regexp typo (!?); 2001-08-03 David Aspinall * CHANGES: Note about improved win32 support * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/fileshow.php: Fix link back to fileshow.php * html/fileshow.html: Renamed file * html/main.html: Fix screenshot link 2001-08-01 David Aspinall * doc/ProofGeneral.texi, doc/PG-adapting.texi: Update last updated, copyright * README.windows: Formatting * README: Update for 3.3 * ChangeLog: Updated. * html/screenshot.html, html/about.html, html/oldnews.html: Fix links to gallery * html/gallery.html: Deleted files. * html/gallery: Renamed file * html/gallery.html: Moved to .php * html/about.html: Fix typo * html/gallery.php, html/gallery.html: Renamed file * html/news.html: Added news * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * generic/proof-autoloads.el: Regenerate to remove Christophes patch * generic/proof-compat.el, generic/proof-site.el: Moved compat hack to proof-site * generic/proof-toolbar.el: Revert to removing and re-adding specifiers for toolbar, so that enablers work at least as well as they did before... * generic/proof-compat.el: Add a dummy version of package-provide for FSFEmacs. 2001-07-25 Christophe Raffalli * generic/proof-autoloads.el, generic/proof-splash.el, README.windows: *** empty log message *** * phox/phox.el, phox/phox-sym-lock.el, phox/phox-fun.el, generic/proof-splash.el, generic/proof-toolbar.el: Various changes for win32 compatibility 2001-07-23 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-menu.el: Prevent error msg in proof-display-some-buffers if response dead. * generic/proof-shell.el: Bug report from Robert Schneck. Make proof-shell-restart start shell. Goals display convention, not hack. 2001-07-09 David Aspinall * ChangeLog: Updated. * todo: TODO for proof-ass fixing added. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-toolbar.el: Clean for compile * generic/proof-menu.el: Clean for compile: new autload * generic/proof-autoloads.el: Refresh * generic/pg-xml.el, generic/pg-user.el: Clean-up compile * generic/proof-compat.el: Add require for arch flags, cleaner compilation. * generic/pg-pgip.el: Fix some bugs shown by byte comp * generic/proof-autoloads.el: Updated autoloads * generic/_pkg.el: Package file (old attempt -- not working) 2001-06-22 Christophe Raffalli * phox/phox.el: *** empty log message *** 2001-05-29 David Aspinall * html/main.html: Fix Coq link. * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * isa/Example.ML: Remove extra proof." * generic/proof-splash.el: Display screen only if called interactively * doc/ProofGeneral.texi: AF2 -> PhoX name change * etc/ProofGeneral.spec: Add REGISTER to doc files. * COPYING: Date 2001 * html/features.html: Fix layout and typo. * html/mailinglist.html: Include PHP file * REGISTER: Note about mailing list and registration. * html/mailinglist, html/mailinglist.php: Renamed file * html/mailinglist.html, html/mailinglist.php: PHP version. Also dont mention junk filters. 2001-05-18 Markus Wenzel * isar/isar-keywords.el: preliminary addition of "corollary"; 2001-05-16 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * doc/ProofGeneral.texi: Minor * bin/proofgeneral: Run the display splash command * generic/proof-config.el: Moved splash settings and basic custom groups elsewhere * CHANGES: splash changes. * generic/proof-site.el: Move loading of compatibility flag, autoloads, basic customization groups here. * generic/proof.el: Move autoloads loads to proof-site, invoke (proof-splash-message) * generic/proof-compat.el: Move emacs version compatibility flags to proof-site.el * generic/proof-splash.el: Move configuration from proof-config here. Make proof-splash-message display logo or print message. * etc/README: Doc of spec and menu, patch now removed 2001-05-08 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.menu: Fix case to match Mandrake menu. * ChangeLog: Updated. * etc/ProofGeneral.menu: Fix quotes. * html/functions.php3: Repair link via htmlshow.php * doc/PG-adapting.texi: Change info dir entry to appear next to Proof General entry. * ChangeLog: Updated. * html/develdownload.php: Set version tag for new release. * Makefile.devel: Change DEVELDOWNLOAD to edit correct file * ChangeLog: Updated. * etc/ProofGeneral.spec: Add a line to clear out build root. * ChangeLog: Updated. * Makefile.devel: Forgot to make BUILD dir. * ChangeLog: Updated. * Makefile.devel: Fix cut and past tab error * Makefile.devel: rpm target: Clean out rpmtopdir, and make subdirs again. Get full path to tar file * ChangeLog: Updated. * Makefile.devel: Clean out NAME, force link. * ChangeLog: Updated. * Makefile.devel: Include a few files from etc in the distribution, esp .spec file * etc/ProofGeneral.menu: *** empty log message *** * etc/ProofGeneral.patch: Deleted files. * ChangeLog: Updated. * doc/ProofGeneral.texi: Fix section title for makeinfo * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Dont make SRPM any more. Use rpm -tb to build binary package from tarball * CHANGES: Updates * etc/ProofGeneral.spec: Updates, removal of patch so that rpm -ta works * doc/ProofGeneral.texi: Updates for 3.3 * generic/proof-utils.el: Fixes for fontification in Xemacs 21.4 * generic/proof-site.el, generic/proof-syntax.el, generic/proof-shell.el, generic/proof-easy-config.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-config.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, generic/proof-compat.el: Copyright date updated * generic/README: Add Markus to list of authors * html/main.html: preliminary -> experimental * html/develdownload.php: No longer distrib SRPM * html/news.html: New news item 2001-05-03 David Aspinall * generic/proof-splash.el: change for Emacs compatibility and FSF/Xemacs update. Copyright update. * generic/proof-script.el: Emacs fix (extent->span). Copyright update. 2001-05-01 David Aspinall * ChangeLog: Updated. * doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi: Try to disable image for now * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/devel.html: Change link to kit * html/download.html: Change link to register page * html/feedback.html, html/index.shtml: Include php file * html/register, html/kit: Register and kit shortcuts * html/develdownload.html: Include php file * html/functions.php3: Link to php files instead of html * html/links, html/main, html/news, html/about, html/devel, html/doc, html/download, html/features: Include php instead of html * html/smallpage.php, html/htmlshow.php, html/index.php, html/develdownload.php, html/feedback.php, html/fileshow.php: Rename some html files php * html/index.html: Deleted files. 2001-04-10 Pierre Courtieu * coq/coq.el: Modification of proof-script-command-end-regexp to allow commands ended by ".eof" 2001-03-20 David Aspinall * ChangeLog: Updated. * html/main.html: Fixes to main page * html/footer.html: Change to my canonical www.dcs web address * html/main.html: Remove proofgeneral.org on main page * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.html: Set version tag for new release. * BUGS: strange buffer selection bug reported by Markus * doc/PG-adapting.texi: Updated magic 2001-03-20 Pierre Courtieu * coq/coq.el: Added the config var proof-script-command-end-regexp fot coq V7. 2001-03-20 David Aspinall * doc/Makefile.doc: Use PS fonts in PS file * generic/proof-shell.el: Remove temporary comments * generic/proof-config.el: Fix docstring * html/feedback.html, html/footer.html, html/functions.php3: Changes to use proofgen@dcs for now instead of broken proofgeneral.org * html/main.html: Fix to Coq web page 2001-03-19 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-26 Pierre Courtieu * coq/coq.el: minor change in coq.el to allow to force version of coq, with variable coq-version-is-V7 2001-02-20 Christophe Raffalli * phox/phox.el, phox/example.phx, phox/phox-extraction.el, phox/phox-fun.el, phox/phox-tags.el, html/develdownload.html, html/devel.html, phox/README, generic/proof-site.el, etc/ProofGeneral.spec: *** empty log message *** 2001-02-08 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-07 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: Set version tag for new release. 2001-02-07 Christophe Raffalli * phox/phox.el, phox/phox-font.el, phox/phox-fun.el, phox/phox-tags.el, phox/phox-extraction.el: *** empty log message *** 2001-02-06 David Aspinall * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-02-02 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-01 Markus Wenzel * doc/ProofGeneral.texi: updated thms_containing; 2001-02-01 Christophe Raffalli * phox/phox-sym-lock.el, phox/phox.el, phox/phox-font.el: *** empty log message *** 2001-01-24 Markus Wenzel * isa/x-symbol-isabelle.el: renamed \ to \ and \ to \; 2001-01-18 Markus Wenzel * isar/isar.el: proof-xsym-deactivate-command: use Library.gen_rems (op =) to avoid \\\\; 2001-01-18 Christophe Raffalli * phox/phox-extraction.el, phox/phox.el, phox/phox-fun.el, phox/phox-tags.el: *** empty log message *** 2001-01-12 Markus Wenzel * isa/isa.el: proof-string-match; 2001-01-12 David Aspinall * ChangeLog: Updated. * isa/isa.el: Fix loading thy mode fist problem: require proof-script since context menus are now added for response/goals buffer, which requires proof mode. 2001-01-12 Markus Wenzel * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: proof-string-match; 2001-01-12 Markus Wenzel * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: proof-string-match; 2001-01-11 Christophe Raffalli * phox/phox.el: *** empty log message *** 2001-01-11 Markus Wenzel * generic/proof-shell.el, generic/pg-xml.el, generic/proof-script.el: fixed format strings in message, error, etc. 2001-01-10 Markus Wenzel * isar/isar-syntax.el: proper font-lock of isar-keywords-proof-heading; * isa/x-symbol-isabelle.el: added \; 2001-01-09 Markus Wenzel * isa/x-symbol-isabelle.el: added \, \, \, \; 2001-01-05 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: Set version tag for new release. 2001-01-03 Markus Wenzel * isar/isar-keywords.el: added "recdef_tc";