diff options
Diffstat (limited to 'ChangeLog')
| -rw-r--r-- | ChangeLog | 2474 |
1 files changed, 2474 insertions, 0 deletions
diff --git a/ChangeLog b/ChangeLog new file mode 100644 index 00000000..56defa21 --- /dev/null +++ b/ChangeLog @@ -0,0 +1,2474 @@ +2002-02-14 David Aspinall <da@proofgeneral.org> + + * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: + Set version tag for new release. + +2002-02-12 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar.el: + more robust proof-shell-interrupt-regexp and proof-shell-error-regexp; + +2002-01-31 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-keywords.el: tuned comment; + +2002-01-21 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/isabelle-system.el: + full-proofs setting; + + * isa/README, isar/README: + Isabelle2002 instead of Isabelle2001; + +2002-01-17 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> + + * phox/.cvsignore: + *** empty log message *** + +2002-01-16 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * etc/isar/trace_simp.thy: tuned; + + * etc/isar/trace_simp.thy: + some test cases for trace_simp output; + +2002-01-11 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: + Set version tag for new release. + +2001-12-27 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar.el: + do not set proof-shell-quit-cmd (admits persistent sessions); + +2001-12-12 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isar/interface, isa/interface: + incorporate smart X11 font installation (used to be in isatool installfonts); + +2001-12-11 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isa/x-symbol-isabelle.el: + \<euro> symbol; + use previously defined x-symbol-isabelle-user-table (or nil); + x-symbol-user-table achieves electric |- and |= symbols; + +2001-11-24 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isar/isar.el: + proof-shell-spill-output-regexp temporarily disabled; + +2001-11-20 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isa/interface, isar/interface: + option -k for logic specific isar-keywords file; + +2001-11-08 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/x-symbol-isabelle.el: + added \<index> symbol; + +2001-11-07 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/x-symbol-isabelle.el: + added \<lozenge> and \<struct>; + + * isar/isar-syntax.el: + updated isar-goals-font-lock-keywords; + +2001-10-24 David Aspinall <da@proofgeneral.org> + + * html/main.html: + Fix missing arg to get. + Add Paul Roziere as req'd by Christopphe Raffalli + +2001-10-13 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-syntax.el: + isar-goals-font-lock-keywords: more general goal pattern; + +2001-10-08 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar.el: + added isar-help-induct-rules; + +2001-10-04 David Aspinall <da@proofgeneral.org> + + * CHANGES: Remove note for devel + + * generic/proof-toolbar.el: + Fix fudged enabler to call button function interactively. + +2001-09-26 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/x-symbol-isabelle.el: + support \<^bold> control symbols; + + * generic/proof-config.el: + fixed spelling; + +2001-09-24 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-syntax.el: + isar-goals-font-lock-keywords: corollary; + +2001-09-10 David Aspinall <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-syntax.el: + isar-goals-font-lock-keywords: corollary; + +2001-09-09 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isa/interface, isar/interface: + tuned usage; + +2001-09-05 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-keywords.el: + new commands (proof terms, code generator); + +2001-08-31 David Aspinall <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * doc/PG-adapting.texi, doc/ProofGeneral.texi: + Fix web page for kit + +2001-08-28 Pierre Courtieu <courtieu@lri.fr> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * html/gallery.php: + Fix screenshots link + + * html/gallery: Fix again. + + * html/gallery: Fix link + +2001-08-10 David Aspinall <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isa/x-symbol-isabelle.el: + fixed potential regexp typo (!?); + +2001-08-03 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <Christophe.Raffalli@univ-savoie.fr> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <Christophe.Raffalli@univ-savoie.fr> + + * phox/phox.el: + *** empty log message *** + +2001-05-29 David Aspinall <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-keywords.el: + preliminary addition of "corollary"; + +2001-05-16 David Aspinall <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <da@proofgeneral.org> + + * 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 <courtieu@lri.fr> + + * coq/coq.el: + Modification of proof-script-command-end-regexp to allow commands + ended by ".eof" + +2001-03-20 David Aspinall <da@proofgeneral.org> + + * 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 <courtieu@lri.fr> + + * coq/coq.el: + Added the config var proof-script-command-end-regexp fot coq V7. + +2001-03-20 David Aspinall <da@proofgeneral.org> + + * 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 <Christophe.Raffalli@univ-savoie.fr> + + * phox/phox-font.el: + *** empty log message *** + +2001-02-26 Pierre Courtieu <courtieu@lri.fr> + + * 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 <Christophe.Raffalli@univ-savoie.fr> + + * 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 <Christophe.Raffalli@univ-savoie.fr> + + * phox/phox-font.el: + *** empty log message *** + +2001-02-07 David Aspinall <da@proofgeneral.org> + + * 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 <Christophe.Raffalli@univ-savoie.fr> + + * 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 <da@proofgeneral.org> + + * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: + Set version tag for new release. + +2001-02-02 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> + + * phox/phox-font.el: + *** empty log message *** + +2001-02-01 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * doc/ProofGeneral.texi: + updated thms_containing; + +2001-02-01 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> + + * phox/phox-sym-lock.el, phox/phox.el, phox/phox-font.el: + *** empty log message *** + +2001-01-24 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/x-symbol-isabelle.el: + renamed \<ll> to \<lless> and \<gg> to \<ggreater>; + +2001-01-18 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isar/isar.el: + proof-xsym-deactivate-command: use Library.gen_rems (op =) to avoid \\\\; + +2001-01-18 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> + + * phox/phox-extraction.el, phox/phox.el, phox/phox-fun.el, phox/phox-tags.el: + *** empty log message *** + +2001-01-12 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/isa.el: proof-string-match; + +2001-01-12 David Aspinall <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: + proof-string-match; + +2001-01-12 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: + proof-string-match; + +2001-01-11 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> + + * phox/phox.el: + *** empty log message *** + +2001-01-11 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * generic/proof-shell.el, generic/pg-xml.el, generic/proof-script.el: + fixed format strings in message, error, etc. + +2001-01-10 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-syntax.el: + proper font-lock of isar-keywords-proof-heading; + + * isa/x-symbol-isabelle.el: + added \<wrong>; + +2001-01-09 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + + * isa/x-symbol-isabelle.el: + added \<cedilla>, \<dieresis>, \<acute>, \<hungarumlaut>; + +2001-01-05 David Aspinall <da@proofgeneral.org> + + * 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 <wenzelm@informatik.tu-muenchen.de> + + * isar/isar-keywords.el: + added "recdef_tc"; + |