diff options
| author | David Aspinall | 2001-08-31 11:44:38 +0000 |
|---|---|---|
| committer | David Aspinall | 2001-08-31 11:44:38 +0000 |
| commit | 784c4ce5a05d54ab9da3902a46c7ad67bac5daa4 (patch) | |
| tree | fd997a6e4c789d963f931df5c1765651de095a77 /ChangeLog | |
| parent | 2fdfaf38ccd283def8febc4ad70844107f659225 (diff) | |
Remove duplicate entries
Diffstat (limited to 'ChangeLog')
| -rw-r--r-- | ChangeLog | 5082 |
1 files changed, 0 insertions, 5082 deletions
@@ -82,34 +82,6 @@ * html/header.html, html/proofgen.css: Improve stylesheet syntax, make menubar smaller -2001-08-28 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-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. @@ -130,44 +102,6 @@ * generic/proof-utils.el: Fix bug in proof-display-and-keep-buffer which had resulted in switching minibuffer windows buffer. -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-17 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-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. @@ -202,38 +136,6 @@ * generic/pg-user.el: Function name fixes, use idiom property in span for popup menu name. -2001-08-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. - - * 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: @@ -285,76 +187,6 @@ * CHANGES: Note of bug fix for buffer-syntactic-context -2001-08-10 David Aspinall <da@proofgeneral.org> - - * 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-10 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: - 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: @@ -377,18 +209,6 @@ * html/main.html: Fix screenshot link -2001-08-03 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/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: @@ -434,60 +254,6 @@ * generic/proof-compat.el: Add a dummy version of package-provide for FSFEmacs. -2001-08-01 David Aspinall <da@proofgeneral.org> - - * 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-08-01 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/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: @@ -509,17 +275,6 @@ * generic/proof-shell.el: Bug report from Robert Schneck. Make proof-shell-restart start shell. Goals display convention, not hack. -2001-07-23 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-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. @@ -553,37 +308,6 @@ * generic/_pkg.el: Package file (old attempt -- not working) -2001-07-09 David Aspinall <da@proofgeneral.org> - - * 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: @@ -626,39 +350,6 @@ * html/mailinglist.html, html/mailinglist.php: PHP version. Also dont mention junk filters. -2001-05-29 David Aspinall <da@proofgeneral.org> - - * 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: @@ -696,36 +387,6 @@ * etc/README: Doc of spec and menu, patch now removed -2001-05-16 David Aspinall <da@proofgeneral.org> - - * 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. @@ -821,595 +482,6 @@ * html/news.html: New news item -2001-05-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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-08 David Aspinall <da@proofgeneral.org> - - * 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: @@ -1453,39 +525,6 @@ * html/index.html: Deleted files. -2001-05-01 David Aspinall <da@proofgeneral.org> - - * 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: @@ -1535,121 +574,6 @@ * html/main.html: Fix to Coq web page -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-20 David Aspinall <da@proofgeneral.org> - - * 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-20 David Aspinall <da@proofgeneral.org> - - * 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: @@ -1683,16 +607,6 @@ * phox/phox.el, phox/phox-font.el, phox/phox-fun.el, phox/phox-tags.el, phox/phox-extraction.el: *** empty log message *** -2001-02-07 David Aspinall <da@proofgeneral.org> - - * 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: @@ -1745,76 +659,11 @@ * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: proof-string-match; -2001-01-12 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -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 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -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 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2001-01-12 David Aspinall <da@proofgeneral.org> - - * 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 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2001-01-12 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-01-11 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> * phox/phox.el: @@ -1845,3939 +694,8 @@ * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: Set version tag for new release. -2001-01-05 David Aspinall <da@proofgeneral.org> - - * 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"; -2000-12-28 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: - include x-symbol-isabelle-font-lock-keywords in shell/goals/response buffers; - more robust \<^sync>; - - * isar/isar-syntax.el: - improved isar-string regexp; - - * isa/x-symbol-isabelle.el: - x-symbol-isabelle-match-subscript: check (proof-ass x-symbol-enable); - -2000-12-23 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: tuned font lock; - -2000-12-22 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-12-22 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * phox/phox.el: - *** empty log message *** - -2000-12-22 David Aspinall <da@proofgeneral.org> - - * generic/proof-script.el: - Removed accidently committed debugging code - -2000-12-22 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * phox/phox.el, phox/example.phx, phox/phox-font.el, generic/proof-script.el: - *** empty log message *** - -2000-12-21 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * phox/phox.el: - *** empty log message *** - -2000-12-21 David Aspinall <da@proofgeneral.org> - - * phox/phox-fun.el: 'goalsave -> 'proof - -2000-12-21 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * phox/phox.el, phox/phox-font.el, phox/phox-fun.el: - *** empty log message *** - -2000-12-21 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. - - * etc/ProofGeneral.spec: .phox -> .phx - - * phox/example.af2, phox/example.phx: - Renamed file - -2000-12-21 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: - Set version tag for new release. - - * etc/ProofGeneral.spec: .phox -> .phx - - * phox/example.af2, phox/example.phx: - Renamed file - -2000-12-20 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * doc/PG-adapting.texi: Fix magic - - * generic/proof-shell.el: - Fix comment to not break texi magic - - * generic/texi-docstring-magic.el: - More broken escapes. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: - Set version tag for new release. - - * CHANGES: Mentioned important changes - - * lego/lego.el, isar/isar.el, generic/pg-user.el: - goalsave -> proof - - * coq/coq.el: - Experimental support for multiple file handling. - 'goalsave -> 'proof - - * doc/PG-adapting.texi: - Document proof-shell-last-output and friends - - * phox/phox-sym-lock.el, phox/sym-lock.el: - Renamed file - - * generic/proof-site.el: - Testing line for PGIP. - - * generic/proof-shell.el: - Improvements to span handling, including new variables: proof-shell-last-output-kind and friends - - * generic/proof-script.el: - Improvements to span handling - -2000-12-20 David Aspinall <da@proofgeneral.org> - - * doc/PG-adapting.texi: Fix magic - - * generic/proof-shell.el: - Fix comment to not break texi magic - - * generic/texi-docstring-magic.el: - More broken escapes. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: - Set version tag for new release. - - * CHANGES: Mentioned important changes - - * lego/lego.el, isar/isar.el, generic/pg-user.el: - goalsave -> proof - - * coq/coq.el: - Experimental support for multiple file handling. - 'goalsave -> 'proof - - * doc/PG-adapting.texi: - Document proof-shell-last-output and friends - - * phox/phox-sym-lock.el, phox/sym-lock.el: - Renamed file - - * generic/proof-site.el: - Testing line for PGIP. - - * generic/proof-shell.el: - Improvements to span handling, including new variables: proof-shell-last-output-kind and friends - - * generic/proof-script.el: - Improvements to span handling - -2000-12-19 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * phox/phox.el, phox/sym-lock.el, phox/phox-font.el, phox/phox-fun.el: - *** empty log message *** - -2000-12-15 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * html/main.html: rename af2 -> Phox - - * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: - Set version tag for new release. - -2000-12-15 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - tuned some (rarely used) symbols; - -2000-12-15 David Aspinall <da@proofgeneral.org> - - * html/main.html: rename af2 -> Phox - - * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: - Set version tag for new release. - -2000-12-15 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - tuned some (rarely used) symbols; - -2000-12-14 David Aspinall <da@proofgeneral.org> - - * generic/proof-script.el: - Remove some user-level functions to pg-user. - Fix bug in proof-goto-end-of-locked. - - * generic/proof-config.el: - Add proof-disappearing-proofs - Make proofs visible command - pg-insert-output-as-comment-fn hook - Alter docstrings for functions using proof-format-filename - - * generic/proof-syntax.el: - Generalise proof-format-filename - - * generic/pg-user.el: - Factor out some material from proof-script.el - - * generic/proof-menu.el: - Add bindings for pg-insert-last-output-as-comment and proof-disappearing-proofs-toggle - - * generic/proof-toolbar.el: - Add visible enable command - - * generic/span-extent.el, generic/span-overlay.el: - Add span-object, mapcar-spans - - * etc/coq/multiple/.cvsignore: - *** empty log message *** - - * etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/c.v, etc/coq/multiple/README: - Updated to use Require commands - -2000-12-07 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * generic/pg-pgip.el: Typo. - - * etc/ProofGeneral.spec, Makefile, Makefile.devel: - Name change af2 -> phox - - * generic/pg-pgip.el: - Beginnings of pgip processing - - * generic/pg-xml.el: Add provide - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-12-07 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * generic/pg-pgip.el: Typo. - - * etc/ProofGeneral.spec, Makefile, Makefile.devel: - Name change af2 -> phox - - * generic/pg-pgip.el: - Beginnings of pgip processing - - * generic/pg-xml.el: Add provide - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-12-07 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * generic/pg-pgip.el: Typo. - - * etc/ProofGeneral.spec, Makefile, Makefile.devel: - Name change af2 -> phox - - * generic/pg-pgip.el: - Beginnings of pgip processing - - * generic/pg-xml.el: Add provide - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-12-07 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * generic/pg-pgip.el: Typo. - - * etc/ProofGeneral.spec, Makefile, Makefile.devel: - Name change af2 -> phox - - * generic/pg-pgip.el: - Beginnings of pgip processing - - * generic/pg-xml.el: Add provide - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-12-07 David Aspinall <da@proofgeneral.org> - - * generic/pg-pgip.el: Typo. - - * etc/ProofGeneral.spec, Makefile, Makefile.devel: - Name change af2 -> phox - - * generic/pg-pgip.el: - Beginnings of pgip processing - - * generic/pg-xml.el: Add provide - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-12-07 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-12-06 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * generic/proof-script.el: - fixed format strings for (message ...); - - * isar/isar-syntax.el: - tuned font-lock-keywords; - -2000-12-01 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - isabelle-command-line: getenv "ISABELLE_OPTIONS"; - - * isar/interface, isa/interface: - added -m option; - -2000-12-01 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * phox/phox.el, phox/sym-lock.el, phox/phox-outline.el, phox/phox-tags.el, phox/phox-font.el, phox/phox-fun.el, phox/example.af2, phox/README, af2/sym-lock.el, af2/phox.el, af2/phox-tags.el, af2/phox-outline.el, af2/phox-font.el, af2/phox-fun.el, af2/example.af2, af2/README, README, generic/proof-site.el, af2/af2.el, af2/af2-outline.el, af2/af2-tags.el, af2/af2-fun.el, af2/af2-font.el: - af2 is now called PhoX - -2000-12-01 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec: - Change info globs to work with mandrake - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - - * doc/ProofGeneral.texi, doc/PG-adapting.texi: - 3.2 -> 3.3pre - -2000-12-01 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2-font.el, af2/af2-fun.el: - add rewrite list - - * af2/af2.el, af2/af2-font.el, af2/af2-fun.el: - *** empty log message *** - -2000-12-01 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec: - Change info globs to work with mandrake - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - - * doc/ProofGeneral.texi, doc/PG-adapting.texi: - 3.2 -> 3.3pre - -2000-12-01 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2-font.el, af2/af2-fun.el: - add rewrite list - - * af2/af2.el, af2/af2-font.el, af2/af2-fun.el: - *** empty log message *** - -2000-12-01 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec: - Change info globs to work with mandrake - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - - * doc/ProofGeneral.texi, doc/PG-adapting.texi: - 3.2 -> 3.3pre - -2000-12-01 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2-font.el, af2/af2-fun.el: - add rewrite list - - * af2/af2.el, af2/af2-font.el, af2/af2-fun.el: - *** empty log message *** - -2000-12-01 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec: - Change info globs to work with mandrake - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - - * doc/ProofGeneral.texi, doc/PG-adapting.texi: - 3.2 -> 3.3pre - -2000-12-01 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2-font.el, af2/af2-fun.el: - add rewrite list - - * af2/af2.el, af2/af2-font.el, af2/af2-fun.el: - *** empty log message *** - -2000-12-01 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - - * doc/ProofGeneral.texi, doc/PG-adapting.texi: - 3.2 -> 3.3pre - -2000-12-01 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2-font.el, af2/af2-fun.el: - add rewrite list - - * af2/af2.el, af2/af2-font.el, af2/af2-fun.el: - *** empty log message *** - -2000-11-27 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * coq/README: fixed spelling; - -2000-11-24 Pierre Courtieu <courtieu@lri.fr> - - * coq/coq.el: - Continuing Coq V7 compatibility work, Begin Silent -> Set Silent, etc... - - * coq/coq.el: - Add a little change to coq-find-and-forget to work better - -2000-11-24 David Aspinall <da@proofgeneral.org> - - * generic/proof-shell.el, generic/proof-config.el: - Added proof-shell-match-pgip-cmd - - * generic/pg-pgip.el: Update branch - - * generic/pg-xml.el: - Added pg-xml-parse-string function. - - * generic/pg-pgip.el: - Functions to process pgip commands. - -2000-11-23 Pierre Courtieu <courtieu@lri.fr> - - * coq/coq.el, coq/coq-syntax.el: - I am starting to make PG coqV7 compatible, I think the best is to - allow both V6 and V7 for a while. Theoretically, incompatibilities - will not be numerous. - -2000-11-22 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/interface, isa/interface: - disable trace option; - -2000-11-21 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/interface, isa/interface: - converted from sh back to bash; - use "#!/usr/bin/env bash" as interpreter to determine bash from PATH; - handle spaces in file names; - -2000-11-17 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - -2000-11-15 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - -2000-11-15 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2.el, af2/af2-font.el, af2/af2-fun.el: - *** empty log message *** - -2000-11-13 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/sym-lock.el, doc/PG-adapting.texi: - *** empty log message *** - -2000-11-10 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * doc/docstring-magic.el, doc/PG-adapting.texi, af2/sym-lock.el: - *** empty log message *** - -2000-10-31 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - tuned isar-goals-font-lock-keywords; - -2000-10-30 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - tuned font-lock-keywords; - - * isa/x-symbol-isabelle.el: - replaced \<macron> by \<inverse> (better than nothing); - -2000-10-30 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * generic/proof-utils.el, generic/proof-script.el, generic/proof-config.el, af2/example.af2, af2/af2.el, af2/af2-fun.el: - *** empty log message *** - -2000-10-27 David Aspinall <da@proofgeneral.org> - - * CHANGES: Ready for 3.2 changes. - -2000-10-27 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/example.af2, generic/proof-utils.el, generic/proof-script.el: - *** empty log message *** - -2000-10-26 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - font-lock support for antiquotations; - -2000-10-26 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * generic/proof-utils.el, af2/af2.el, af2/af2-fun.el, af2/example.af2: - *** empty log message *** - -2000-10-19 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: - Set version tag for new release. - - * Makefile.devel: - Second part of moving to 3.3pre series. - -2000-10-19 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * Makefile.devel: - Second part of moving to 3.3pre series. - -2000-10-18 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. - - * Makefile.devel: - Begin move to 3.3 series. - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * html/register.html: Fix parse error. - -2000-10-18 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. - - * Makefile.devel: - Begin move to 3.3 series. - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * html/register.html: Fix parse error. - -2000-10-18 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * Makefile.devel: - Begin move to 3.3 series. - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * html/register.html: Fix parse error. - -2000-10-18 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * html/register.html: Fix parse error. - -2000-10-14 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - parendblleft/right renamed to cataleft/right (according to x-symbol-3.3e); - -2000-10-12 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - support for super- and subscripts (still needs proper per-prover - control of x-symbol-subscripts variable); - -2000-10-03 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. - - * html/download.html: - Apparently X-Sym web pages have simpler install instructions now. - -2000-10-02 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - added settings: eta-contract, goals-limit, prems-limit; - -2000-10-03 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * html/download.html: - Apparently X-Sym web pages have simpler install instructions now. - -2000-10-02 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - added settings: eta-contract, goals-limit, prems-limit; - -2000-10-02 David Aspinall <da@proofgeneral.org> - - * etc/announce: - Removed link to CHANGES, its buggy - - * ChangeLog: Updated. - - * todo: Updated - - * ChangeLog: - Remove more duplicate entries. - - * etc/release-log.txt: 3-2-1 pending - - * Makefile.devel: - Warning about duplicate ChangeLog entries - - * Makefile.devel: - Tweak to ChangeLog production - - * ChangeLog: Remove duplicate entries. - - * ChangeLog: Updated. - - * etc/announce: - Mention Isabelle99-1 change - - * etc/ProofGeneral.spec, generic/proof-site.el: - Set version tag for new release. - - * CHANGES: - Whoops, left pre-release header in - - * etc/release-log.txt: - Upcoming patch anticipated already. - - * doc/Makefile.doc: Fix recursive make - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.html: - Set version tag for new release. - - * html/develdownload.html: - Note about current pre-release being outdated wrt 3.2 - - * ChangeLog: Updated. - - * todo: Updated - - * Makefile.devel: - Remove ps and pdf for PG-adapting from distrib to redue size to normal proportions. - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, generic/proof-site.el: - Set version tag for new release. - - * etc/release-log.txt: - Add todays date, 3.2 - - * html/doc.html, html/download.html, html/index.html, html/news.html, html/oldnews.html: - Updated web pages for 3.2 release - - * todo: Updated, cleaned up - - * coq/coqtags, lego/legotags: - Note about alternative path to perl - - * doc/PG-adapting.texi: Updated magic - - * INSTALL: Caveats about using elcs. - - * af2/README: New file - - * bin/proofgeneral: - Pass extra args to emacs. - - * doc/Makefile.doc: - Attempt to force image build - - * doc/PG-adapting.texi: Subtitle caps - -2000-10-02 David Aspinall <da@proofgeneral.org> - - * todo: Updated - - * ChangeLog: - Remove more duplicate entries. - - * etc/release-log.txt: 3-2-1 pending - - * Makefile.devel: - Warning about duplicate ChangeLog entries - - * Makefile.devel: - Tweak to ChangeLog production - - * ChangeLog: Remove duplicate entries. - - * ChangeLog: Updated. - - * etc/announce: - Mention Isabelle99-1 change - - * etc/ProofGeneral.spec, generic/proof-site.el: - Set version tag for new release. - - * CHANGES: - Whoops, left pre-release header in - - * etc/release-log.txt: - Upcoming patch anticipated already. - - * doc/Makefile.doc: Fix recursive make - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.html: - Set version tag for new release. - - * html/develdownload.html: - Note about current pre-release being outdated wrt 3.2 - - * ChangeLog: Updated. - - * todo: Updated - - * Makefile.devel: - Remove ps and pdf for PG-adapting from distrib to redue size to normal proportions. - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, generic/proof-site.el: - Set version tag for new release. - - * etc/release-log.txt: - Add todays date, 3.2 - - * html/doc.html, html/download.html, html/index.html, html/news.html, html/oldnews.html: - Updated web pages for 3.2 release - - * todo: Updated, cleaned up - - * coq/coqtags, lego/legotags: - Note about alternative path to perl - - * doc/PG-adapting.texi: Updated magic - - * INSTALL: Caveats about using elcs. - - * af2/README: New file - - * bin/proofgeneral: - Pass extra args to emacs. - - * doc/Makefile.doc: - Attempt to force image build - - * doc/PG-adapting.texi: Subtitle caps - -2000-09-29 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/proofgeneral-domain.txt: - Added a new email alias - - * doc/PG-adapting.texi: - Typos in credits section - - * doc/PG-adapting.texi: - Added credits section - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec: - Another buglet in files list - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec: - Bug in files list - - * ChangeLog: Updated. - - * .cvsignore: - Remove ChangeLog from ignoreds - - * Makefile.devel, ChangeLog: - Fix ChangeLog target so makes prefix properly. Revert to keeping uncompressed file in repo. - - * Makefile, Makefile.devel: - Add acl2 and twelf to elisp dirs - - * etc/ProofGeneral.spec: - Fix adding acl2 and twelf to RPM - - * Makefile.devel: - ChangeLog is just last 1000 lines, instead of 11000 starting in 1996... - - * html/smallheader.html, html/header.html: - Link image to root dir. - - * html/main.html: Tweak - - * etc/ProofGeneral.patch: - Remove patch on perl filename now, after Pierres accidental checkin. - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/twelf-old.el, twelf/README, twelf/example.elf, twelf/twelf-font.el, plastic/plastic.el, plastic/test.lf, plastic/todo, papers/README, plastic/README, plastic/plastic-syntax.el, lego/legotags, lego/readonly/readonly.l, lego/todo, lego/x-symbol-lego.el, lego/example2.l, lego/lego-syntax.el, lego/lego.el, lego/BUGS, lego/README, lego/example.l, isar/isar.el, isar/todo, isar/interface, isar/isar-keywords.el, isar/isar-syntax.el, isar/BUGS, isar/Example.thy, isar/README, isa/thy-mode.el, isa/todo, isa/x-symbol-isabelle.el, isa/isa.el, isa/isabelle-system.el, isa/interface, isa/interface-setup.el, isa/isa-syntax.el, isa/Example.thy, isa/Example2.ML, isa/README, isa/depends.ML, isa/BUGS, isa/Example-Xsym.ML, isa/Example.ML, images/gimp/.cvsignore, images/gimp/scripts/proofgeneral.scm, images/use.xpm, images/undo.xcf, images/undo.xpm, images/use.8bit.xpm, images/use.xcf, images/state.8bit.xpm, images/state.xcf, images/state.xpm, images/undo.8bit.xpm, images/retract.8bit.xpm, images/retract.xcf, images/retract.xpm, images/restart.8bit.xpm, images/restart.xcf, images/restart.xpm, images/pgmini.xpm, images/qed.8bit.xpm, images/qed.xcf, images/qed.xpm, images/pgicon.png, images/pg-text.gif, images/pg-text.jpg, images/pg-text.xcf, images/next.xpm, images/notes.txt, images/pg-text.8bit.gif, images/next.8bit.xpm, images/next.xcf, images/isabelle_transparent.gif, images/isabelle_transparent.xcf, images/lego-badge.xcf, images/isabelle_transparent.8bit.gif, images/interrupt.8bit.xpm, images/interrupt.xcf, images/interrupt.xpm, images/isabelle-badge.xcf, images/help.xpm, images/info.8bit.xpm, images/info.xcf, images/info.xpm, images/goto.xcf, images/goto.xpm, images/help.8bit.xpm, images/help.xcf, images/goto.8bit.xpm, images/goal.xcf, images/goal.xpm, images/goal_large.xcf, images/fireworks.xcf, images/goal.8bit.xpm, images/find.8bit.xpm, images/find.xcf, images/find.xpm, images/context.xpm, images/coq-badge.xcf, images/command.xcf, images/command.xpm, images/context.8bit.xpm, images/context.xcf, images/abort.xcf, images/abort.xpm, images/blank.xcf, images/command.8bit.xpm, images/README, images/abort.8bit.xpm, images/ProofGeneral.jpg, images/ProofGeneral.xcf, images/Makefile, images/ProofGeneral.8bit.gif, images/ProofGeneral.gif, html/projects/thybrowse.html, html/projects/webreplay.html, html/projects/xmlpgip.html, images/.cvsignore, html/projects/pgml.html, html/projects/reelcase.html, html/projects/scrgen.html, html/projects/test.html, html/projects/isapbp.html, html/projects/mm.html, html/projects/outline.html, html/projects/pgip.html, html/projects/coqfile.html, html/projects/coqpbp.html, html/projects/corba.html, html/projects/hol.html, html/projects/acs.html, html/papers/pgtalk.pdf, html/papers/pgoutline.ps.gz, html/papers/pgoutline.pdf, html/images/whole-man-thumb.jpg, html/images/whole-man.jpg, html/images/whip-thumb.jpg, html/images/whip.jpg, html/images/portrait.jpg, html/images/silverrule.gif, html/images/vh40.gif, html/images/pg-lego-thumb.png, html/images/pg-text.gif, html/images/portrait-thumb.jpg, html/images/pg-isar-thumb.png, html/images/pg-lego-console-thumb.png, html/images/pg-lego-console.png, html/images/pg-lego-screenshot.png, html/images/pg-isa-thumb.png, html/images/pg-isar-screenshot.png, html/images/pg-coq-thumb.png, html/images/pg-isa-screenshot.png, html/images/isabelle.gif, html/images/lego-badge.gif, html/images/pg-coq-screenshot.png, html/images/coq-badge.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf, html/images/isabelle-badge.gif, html/images/PG-small.jpg, html/images/ProofGeneral.jpg, html/images/bullethole.gif, html/images/canvaswallpaper.jpg, html/Kit/dtd/pgml.dtd, html/images/.cvsignore, html/images/IsaPGscreen.jpg, html/Kit/dtd/pgip.dtd, html/screenshot.html, html/smallheader.html, html/smallpage.html, html/projects.html, html/proofgen.css, html/register.html, html/screenshot, html/notes.txt, html/oldnews.html, html/oldrel.html, html/main.html, html/mission.html, html/news, html/news.html, html/links, html/links.html, html/mailinglist.html, html/main, html/hits.html, html/htmlshow.html, html/index.html, html/index.shtml, html/kit.html, html/functions.php3, html/gallery.html, html/head.html, html/header.html, html/features.html, html/feedback.html, html/fileshow.html, html/footer.html, html/download.html, html/elispmarkup.php3, html/features, html/develdownload.html, html/doc, html/doc.html, html/download, html/cvsweb.conf, html/devel, html/devel.html, html/about.html, html/counter.php3, html/cvsweb.cgi, html/about, html/ProofGeneralPortrait.eps.gz, hol98/todo, hol98/x-symbol-hol98.el, html/.cvsignore, hol98/example.sml, hol98/hol98.el, generic/span.el, generic/texi-docstring-magic.el, hol98/README, generic/span-extent.el, generic/span-overlay.el, generic/proof-x-symbol.el, generic/proof.el, generic/proof-toolbar.el, generic/proof-utils.el, generic/proof-splash.el, generic/proof-syntax.el, generic/proof-system.el, generic/proof-site.el, generic/proof-shell.el, generic/proof-menu.el, generic/proof-script.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-indent.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/proof-config.el, etc/pgkit/xmltest2.xml, generic/README, generic/pg-xml.el, etc/patches/duplicated-short-messages-fix.txt, etc/patches/fix-attempt-for-eager-cleaning.txt, etc/pgkit/xmltest1.xml, 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/C.thy, etc/isar/multiple/D.thy, etc/isar/multiple/README, etc/lego/GoalGoal.l, etc/isar/README, etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/multiple/A.thy, etc/isar/multiple/B.thy, etc/demoisa/C.ML, etc/demoisa/D.ML, etc/demoisa/README, etc/isar/Parsing.thy, etc/demoisa/A.ML, etc/demoisa/B.ML, etc/isa/thy/test.ML, etc/isa/multiple/Err.ML, etc/isa/multiple/Err.thy, etc/isa/multiple/README, etc/isa/multiple/foobar/foo.ML, etc/isa/multiple/C.thy, etc/isa/multiple/D.ML, etc/isa/multiple/D.thy, etc/isa/multiple/A.thy, etc/isa/multiple/B.ML, etc/isa/multiple/B.thy, etc/isa/multiple/C.ML, etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/multiple/A.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/depends/Fib.ML, etc/isa/long-line-backslash.ML, etc/isa/message-test.ML, etc/isa/settings.ML, etc/isa/xsym.ML, etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/c.v, etc/isa/goal-matching.ML, etc/coq/multiple/README, etc/coq/unnamed_thm.v, etc/proofgeneral-domain.txt, etc/release-log.txt, etc/screenshot-notes.txt, etc/test-schedule.txt, etc/testing-log.txt, etc/doc-notes.txt, etc/junk.el, etc/profiling.txt, etc/cvs-tips.txt, etc/debugging-tips.txt, etc/README, etc/TESTS, etc/announce, etc/bug-notes.txt, etc/ProofGeneral.patch, etc/ProofGeneral.spec, doc/dir, doc/docstring-magic.el, doc/localdir, doc/README.doc, doc/ProofGeneral.jpg, doc/ProofGeneral.texi, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile, doc/Makefile.doc, demoisa/README, demoisa/demoisa-easy.el, demoisa/demoisa.el, coq/example.v, coq/todo, coq/x-symbol-coq.el, coq/coq-syntax.el, coq/coq.el, coq/coqtags, bin/proofgeneral, coq/BUGS, coq/README, af2/af2-tags.el, af2/af2.el, af2/example.af2, af2/sym-lock.el, acl2/x-symbol-acl2.el, af2/af2-font.el, af2/af2-fun.el, af2/af2-outline.el, acl2/README, acl2/acl2.el, acl2/example.acl2, todo, README, README.devel, TODO, Makefile, Makefile.devel, Makefile.xemacs, FAQ, INSTALL, CHANGES, COPYING, AUTHORS, BUGS: - Updating branch - - * etc/cvs-tips.txt: - Note about dealing with backslashname directory. - - * todo: Updated - - * etc/cvs-tips.txt: - Note about dealing with backslashname directory. - - * INSTALL: - Update URLs and mail aliases. Mention script, and extensions for new provers - - * bin/proofgeneral: - Script for launching proofgeneral. - - * todo: Updated - - * etc/ProofGeneral.spec: - Add more provers, and proofgeneral script - - * etc/proofgeneral-domain.txt: - Notes about proofgeneral.org - - * images/pgmini.xpm, images/pgicon.png: - Add icon images. - - * html/develdownload.html: Minor change - - * INSTALL: Note about packages needed - - * html/functions.php3: - Click to go back links to root. - - * html/register.html, html/features.html, html/header.html, html/main.html, html/mission.html, html/oldnews.html, html/projects.html, html/about.html, html/develdownload.html, html/doc.html, html/download.html: - Remove messy link_root links. - - * html/links, html/main, html/news, html/about, html/devel, html/doc, html/download, html/features: - Short file instead of a link, so works in CVS. Bit annoying to duplicate, but never mind. - - * html/about, html/links, html/devel, html/doc, html/screenshot, html/download, html/features, html/news, html/main: - Links for shortcut URLs. - - * html/notes.txt: - Mention needed server hacks - - * html/functions.php3: - Remove link_root nonsense - - * todo: Updated with fixes before 3.2. - - * BUGS: - Inherent problem with Emacs in console mode: no face support - - * Makefile.devel: - twelf and acl2 are in ordinary dist - - * etc/announce: Mention ACL2 too - - * twelf/README: Tweak - - * demoisa/demoisa-easy.el: Comment fix - - * generic/proof-script.el: - Parse comments also in proof-script-generic-parse-sexp - - * generic/proof-menu.el: - Non existent get-window-buffer -> get-buffer-window (how did that get through?) - - * generic/proof-config.el: - Default for proof-comment-end that doesn't cause looping in searching for comment end. - - * acl2/README, acl2/acl2.el, acl2/example.acl2: - Updated, trimmed down to barebones. - -2000-09-29 Pierre Courtieu <courtieu@lri.fr> - - * coq/todo: - added some comments in coq/todo - -2000-09-29 David Aspinall <da@proofgeneral.org> - - * coq/coqtags, lego/legotags: - Make default path to perl be /usr/bin/perl - -2000-09-29 Pierre Courtieu <courtieu@lri.fr> - - * coq/x-symbol-coq.el: - a little change in coq/x-symbol, nothing - - * coq/coq.el: - A little work around for the bug of Coq concerning the restart that - uses Reset Initial which doesn't reset the Implicit Arguments flag to - Off (this is the bug), I added the good command to the coq reset - command, this has to be backtracked when V7 will be done (the bug is - already corrected in V7). - - * lego/legotags, coq/x-symbol-coq.el, coq/coq.el, coq/coqtags, coq/coq-syntax.el: - Added Uncaught exception errors in coq-error-regexp. - -2000-09-29 David Aspinall <da@proofgeneral.org> - - * Makefile, Makefile.devel: - Add acl2 and twelf to elisp dirs - - * etc/ProofGeneral.spec: - Fix adding acl2 and twelf to RPM - - * Makefile.devel: - ChangeLog is just last 1000 lines, instead of 11000 starting in 1996... - - * ChangeLog.gz: Updated. - - * html/smallheader.html, html/header.html: - Link image to root dir. - - * html/main.html: Tweak - - * etc/ProofGeneral.patch: - Remove patch on perl filename now, after Pierres accidental checkin. - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: - Set version tag for new release. - - * All files: - Updating branch - - * etc/cvs-tips.txt: - Note about dealing with backslashname directory. - - * todo: Updated - - * etc/cvs-tips.txt: - Note about dealing with backslashname directory. - - * INSTALL: - Update URLs and mail aliases. Mention script, and extensions for new provers - - * bin/proofgeneral: - Script for launching proofgeneral. - - * todo: Updated - - * etc/ProofGeneral.spec: - Add more provers, and proofgeneral script - - * etc/proofgeneral-domain.txt: - Notes about proofgeneral.org - - * images/pgmini.xpm, images/pgicon.png: - Add icon images. - - * html/develdownload.html: Minor change - - * INSTALL: Note about packages needed - - * html/functions.php3: - Click to go back links to root. - - * html/register.html, html/features.html, html/header.html, html/main.html, html/mission.html, html/oldnews.html, html/projects.html, html/about.html, html/develdownload.html, html/doc.html, html/download.html: - Remove messy link_root links. - - * html/links, html/main, html/news, html/about, html/devel, html/doc, html/download, html/features: - Short file instead of a link, so works in CVS. Bit annoying to duplicate, but never mind. - - * html/about, html/links, html/devel, html/doc, html/screenshot, html/download, html/features, html/news, html/main: - Links for shortcut URLs. - - * html/notes.txt: - Mention needed server hacks - - * html/functions.php3: - Remove link_root nonsense - - * todo: Updated with fixes before 3.2. - - * BUGS: - Inherent problem with Emacs in console mode: no face support - - * Makefile.devel: - twelf and acl2 are in ordinary dist - - * etc/announce: Mention ACL2 too - - * twelf/README: Tweak - - * demoisa/demoisa-easy.el: Comment fix - - * generic/proof-script.el: - Parse comments also in proof-script-generic-parse-sexp - - * generic/proof-menu.el: - Non existent get-window-buffer -> get-buffer-window (how did that get through?) - - * generic/proof-config.el: - Default for proof-comment-end that doesn't cause looping in searching for comment end. - - * acl2/README, acl2/acl2.el, acl2/example.acl2: - Updated, trimmed down to barebones. - -2000-09-29 Pierre Courtieu <courtieu@lri.fr> - - * coq/todo: - added some comments in coq/todo - -2000-09-29 David Aspinall <da@proofgeneral.org> - - * coq/coqtags, lego/legotags: - Make default path to perl be /usr/bin/perl - -2000-09-29 Pierre Courtieu <courtieu@lri.fr> - - * coq/x-symbol-coq.el: - a little change in coq/x-symbol, nothing - - * coq/coq.el: - A little work around for the bug of Coq concerning the restart that - uses Reset Initial which doesn't reset the Implicit Arguments flag to - Off (this is the bug), I added the good command to the coq reset - command, this has to be backtracked when V7 will be done (the bug is - already corrected in V7). - - * lego/legotags, coq/x-symbol-coq.el, coq/coq.el, coq/coqtags, coq/coq-syntax.el: - Added Uncaught exception errors in coq-error-regexp. - -2000-09-28 David Aspinall <da@proofgeneral.org> - - * doc/ProofGeneral.texi, doc/PG-adapting.texi: - Date becomes Oct - - * acl2/acl2.el: Fix web page, at least. - - * ChangeLog.gz: Updated. - - * twelf/README: Notes. - - * doc/ProofGeneral.texi: Tweaks - - * todo, Makefile.devel: - phtml -> html - - * etc/announce: Fix URL. - - * html/download.html, html/index.html: - Renamed files - - * phtml -> html - Renamed files - - * ChangeLog.gz: Updated. - - * twelf/twelf-font.el: Add FIXME - - * generic/proof-script.el: Fix comment. - - * twelf/twelf.el: - Var name change use-new-parsing -> use-new-parser. Turn on font lock by default. - - * doc/ProofGeneral.texi: - Fix typo, add credit. - -2000-09-28 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: isar-web-page; - -2000-09-28 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * doc/Makefile: Add default target - - * acl2/x-symbol-acl2.el, acl2/README, acl2/acl2.el, acl2/example.acl2: - First (non-working) versions, committed so that doc builds. - - * README: Fix date - - * README.devel: Dreams about testing - - * todo: - Generalize Isabelles atomic file scripting. - - * TODO: - Added generic line width adjusting to grand TODO - - * doc/PG-adapting.texi: - Added extra section on how to tweak script input to the shell - - * generic/proof-config.el: - Added proof-shell-strip-crs-from-input, and unadvertised proof-script-fly-past-comments - - * generic/proof-menu.el: - Added fly past comments to quick opts menu when new parsing mechanism active. - - * generic/proof-script.el: - Bug fix in proof-goto-end-of-locked. Comments in new parsing functions. Tweaks to proof-script-generic-parse-cmdstart. Combine fly-past and coelesce comment options. Use proof-string-match-safe in generic-goal-command-p, to avoid error in Twelf. - - * generic/proof-shell.el: - Added proof-shell-strip-crs-from-input. - - * twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/example.elf, twelf/twelf-font.el: - Fixes to twelf support, begins to work now. - -2000-09-28 David Aspinall <da@proofgeneral.org> - - * doc/ProofGeneral.texi, doc/PG-adapting.texi: - Date becomes Oct - - * acl2/acl2.el: Fix web page, at least. - - * ChangeLog.gz: Updated. - - * twelf/README: Notes. - - * doc/ProofGeneral.texi: Tweaks - - * todo, Makefile.devel: - phtml -> html - - * etc/announce: Fix URL. - - * html/*.phtml -> *.html (more) - Moved to use .html instead of .phtml - - * html/download.html, html/index.html: - Renamed files - - * html/*.phtml -> *.html - Renamed files - - * ChangeLog.gz: Updated. - - * twelf/twelf-font.el: Add FIXME - - * generic/proof-script.el: Fix comment. - - * twelf/twelf.el: - Var name change use-new-parsing -> use-new-parser. Turn on font lock by default. - - * doc/ProofGeneral.texi: - Fix typo, add credit. - -2000-09-28 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: isar-web-page; - -2000-09-28 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * doc/Makefile: Add default target - - * acl2/x-symbol-acl2.el, acl2/README, acl2/acl2.el, acl2/example.acl2: - First (non-working) versions, committed so that doc builds. - - * README: Fix date - - * README.devel: Dreams about testing - - * todo: - Generalize Isabelles atomic file scripting. - - * TODO: - Added generic line width adjusting to grand TODO - - * doc/PG-adapting.texi: - Added extra section on how to tweak script input to the shell - - * generic/proof-config.el: - Added proof-shell-strip-crs-from-input, and unadvertised proof-script-fly-past-comments - - * generic/proof-menu.el: - Added fly past comments to quick opts menu when new parsing mechanism active. - - * generic/proof-script.el: - Bug fix in proof-goto-end-of-locked. Comments in new parsing functions. Tweaks to proof-script-generic-parse-cmdstart. Combine fly-past and coelesce comment options. Use proof-string-match-safe in generic-goal-command-p, to avoid error in Twelf. - - * generic/proof-shell.el: - Added proof-shell-strip-crs-from-input. - - * twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/example.elf, twelf/twelf-font.el: - Fixes to twelf support, begins to work now. - -2000-09-27 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/todo: - ** C func-menu: observe proof-syntactic-context (general problem of - func-menu setup?); - - * doc/ProofGeneral.texi: - proper spelling: "Leonor Prensa Nieto"; - fixed @kindex for LEGO and Coq; - Isabelle Proof General: cover Isabelle/Isar as well; - - * isar/isar-syntax.el: - removed broken outline stuff; - - * isar/isar.el: tuned docstring; - -2000-09-27 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * todo: Updated - - * README: Updated, mention PG Kit. - - * Makefile.devel: - proofgeneral email address for me - - * BUGS: Updated - - * doc/PG-adapting.texi: - Added future section, fixed URLs. Updated to mention proof-script-sexp-commands. - - * doc/ProofGeneral.texi: - Shortened BUGs appendix, other improvements - - * coq/BUGS: Updated from doc - - * etc/announce: Updated - - * etc/ProofGeneral.spec: - Fix URL of source - - * html/images/PG-small.jpg: - Already shrunken general for buggy browsers benefit. - - * html/smallheader.phtml, html/mailinglist.phtml, html/main.phtml, html/news.phtml, html/screenshot.phtml, html/doc.phtml, html/feedback.phtml, html/footer.phtml, html/functions.php3, html/header.phtml, html/devel.phtml: - Updated web pages, misc improvements. - - * generic/proof-utils.el: - Fix bug email address to bugs@proofgeneral.org - - * generic/proof-site.el: Added ACL2 - - * generic/proof-config.el, generic/proof-script.el: - Added yet another new parsing mechanism, bit more rational this time. - - * isa/BUGS: - Added bugs that were mentioned in manual - - * isa/isa.el: - Dont use customize-set-variable for add splash logo - - * html/kit.html: - Working home page for PG kit - - * html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd: - Added kit stuff: just copies of the DTDs at the moment. - -2000-09-26 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec: - Fix adding af2 to RPM. - - * Makefile.devel: - Remove extra space preventing ChangeLog update. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * html/main.phtml: - Link to Isar instead of Isar/README. - - * images/goto.xpm: Make backgroundize - - * html/main.phtml: - Fix Pauls web address - - * html/oldnews.phtml, papers/README, html/about.phtml, html/cvsweb.conf, html/devel.phtml, generic/proof-utils.el, etc/ProofGeneral.spec, generic/proof-config.el, doc/README.doc, doc/ProofGeneral.texi, BUGS, FAQ, README, doc/PG-adapting.texi: - Fix Proof General web page to www.proofgeneral.org. - - * etc/announce: Updated for 3.2 release - - * html/develdownload.phtml: Typo - -2000-09-25 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * Makefile.devel: - Remove twelf from .tar.gz - - * etc/ProofGeneral.spec: - Add AF2 to RPM package. - - * isa/todo: - Added bits from todo for Isabelle - -2000-09-25 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - isa-isatool-command: tuned standard places of Isabelle installation; - - * generic/proof-utils.el: - comment: avoid unbalanced quotes; - -2000-09-23 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * TODO: Updated - - * doc/ProofGeneral.texi: Update date. - - * generic/proof-menu.el: - proof-display-some-buffers moves point to end of output in response buffer. - - * html/news.phtml: - Forthcoming news item - - * html/main.phtml: - Use prover-specific logos rather than generic ones... - - * html/header.phtml: - Changed size of image - - * html/develdownload.phtml: Minor - - * todo: Removed: - X Improve efficiency for processing for large proofs (N/A) - D Enable toolbar in other PG buffers (done) - A Add Pierre's improvement for X-Symbol config (done) - A make C-c C-l go to bottom of response buffer while output (done) - B New keymap(s) for proof assistants. (done) - A Add efficiency improvement by turning on/off prover output. (done) - C Make the remaining options in the quick-opts-menu be more (done|N/A) - - * html/images/isabelle.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf: - Add prover-specific logo rather than generic ones... - - * html/images/ProofGeneral.jpg, images/ProofGeneral.jpg: - Image of the general with ??? badge - - * hol98/x-symbol-hol98.el, lego/x-symbol-lego.el: - Add Pierre's tweak - - * twelf/x-symbol-twelf.el: - Standard poor X-Symbol support for twelf. - - * todo: - Changes: (actually in previous version) - - Undoing comments with FSF Emacs fixed (thanks to Christophe Raffalli) - - C-x C-v and C-x C-w supposed fixed. - - have added proof-shell-important-settings - - confused (initialization) bug: assumed fixed. - - proof-shell-handle-error-hook has gone - - rpm relocatability improved - - Added auto-autoloads - - proof-goals-display-qed-message has gone - - added mechanism to close goal....<nosave> goal.... sequences - - Removed unimportant X's: - * X Consider filtering out special annotations from shell buffer - - * images/goto.xbm: Deleted file - - * generic/proof-menu.el: - proof-display-some-buffers improved: toggles between goals and response in - 2-pane mode - - * generic/proof-utils.el: - Fix proof-display-and-keep-buffer for displaying from non-script buffer. Add proof-with-script-buffer. - - * generic/span-overlay.el: - Always activate bug fix -- this file only loaded for FSF Emacs. - - * generic/proof-toolbar.el: - Make toolbar enablers work appropriately from non-scripting buffers - Remove support for obsolete 1-bit xbm images - Update comments - - * generic/proof-shell.el: - Call (proof-toolbar-setup) to add toolbar to goals and response buffer - Unify goals and response menus with script buffer menu - - * images/use.xbm, images/undo.xbm, images/state.xbm, images/retract.xbm, images/restart.xbm, images/qed.xbm: - Deleted file - - * generic/proof-script.el: - Remove require on proof-depends - Make toolbar commands work from non-scripting buffers - Add save file dialogue to proof-register-possibly-new-processed-file - - * images/interrupt.xbm: Deleted file - - * generic/proof-depends.el: - Update comments - - * images/info.xbm: Deleted file - - * generic/README: Updated - - * images/help.xbm, images/goal.xbm: - Deleted file - - * todo, INSTALL, CHANGES, BUGS: - Updated - - * images/find.xbm, images/context.xbm, images/command.xbm, images/abort.xbm, images/next.xbm: - Deleted file - - * images/goto.8bit.xpm, images/goto.xcf, images/goto.xpm: - Improved(?) goto button - - * images/gimp/scripts/proofgeneral.scm: - Remove obsolete xbms - - * images/Makefile: Remove xbm's - -2000-09-21 David Aspinall <da@proofgeneral.org> - - * doc/PG-adapting.texi: - Slightly shorter name for info dir entry. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml: - Set version tag for new release. - - * etc/ProofGeneral.spec: - Fix globbing some more. - - * etc/ProofGeneral.spec: - Fix for rpm braindead globbing. - - * doc/ProofGeneral.texi: - Fix infodir entry, it got broken somehow. - - * etc/ProofGeneral.spec: - Add PG-adapting to info files. - -2000-09-21 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/interface-setup.el: - tweak 'x-symbol-image-converter to avoid confusing warning; - - * isar/interface, isa/interface: - use plain /bin/sh instead of bash; - -2000-09-21 David Aspinall <da@proofgeneral.org> - - * etc/ProofGeneral.spec: - Added Prefixes: tag - - * Makefile.devel: - Add symlink PG -> PG-ver to main dist. Dont dereference symlinks when making tars (why was it done?). - - * doc/Makefile: - Make PG-adapting first so index.html left pointing to main manual - -2000-09-21 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - added Isabelle symbols for parendblleft/parendblright glyphs (will be - present in X-Symbol-3.3e; should not cause problems with older - versions); - -2000-09-21 David Aspinall <da@proofgeneral.org> - - * generic/proof-config.el: Newlines. - - * images/abort.xcf, images/goal.8bit.xpm: - Tweaked abort button - - * doc/PG-adapting.texi: - Improved adding more lisp code chapter. - - * Makefile.devel: - Changed ChangeLog target to use rcs2log directly. Added developer's details, correct emails. - - * generic/proof-compat.el: - Removed blurry distinction between block-comment and comment in FSF's buffer-syntactic-context - -2000-09-21 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/todo: - ** D support proof-next-error? - - * isar/isar.el: tuned comment; - - * etc/isar/README: - bug2: Resolved as of 17.9.00; - - * etc/screenshot-notes.txt: - fixed "Dagstuhl"; - - * todo: done: exit isar; - added comment about output performance; - -2000-09-20 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/interface, isa/interface: - added -X option; - -2000-09-20 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * generic/proof-script.el: Comments - - * generic/proof-config.el: - Disable toolbar enablers on win32. - - * images/abort.8bit.xpm, images/abort.xbm, images/abort.xpm: - New generated buttons. - - * images/gimp/scripts/proofgeneral.scm: - Add new button - -2000-09-20 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * images/Makefile: added abort button - - * images/abort.xcf: abort button - - * generic/span-overlay.el: - dirty bug fix in next-span to avoid loops with FSF Emacs - -2000-09-19 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - made \<> word characters (accomodates symbol representation); - - * isar/interface, isa/interface: - installfonts only when using X window system; - - * isar/isar.el: - isar-toolbar-entries: remove 'goal and 'qed; - - * isar/isar-syntax.el: removed junk; - - * isa/interface-setup.el: - improved xsymbol config: include info dir, only init for XEmacs; - - * isa/todo: - done: ability to choose logic; - - * isar/interface, isa/interface: - isa: DEFAULT_FILES="Scratch.thy Scratch.ML"; - - * isar/README: Isabelle version: 99-1; - tuned; - - * isa/README: Isabelle version: 99-1; - -2000-09-18 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/interface-setup.el: - more robust checking of xsymbol-home; - -2000-09-18 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2-fun.el: - *** empty log message *** - - * generic/proof-utils.el: - changed proof-remove-comment to avoid using string-search (using string-match instead). - -2000-09-18 David Aspinall <da@proofgeneral.org> - - * todo: Updated - - * ChangeLog.gz: Updated. - - * generic/proof-script.el: - Get rid of proof-segment-up-to-old. - - * generic/proof-compat.el: - Added bug fix section and patch for undefined - font-lock-preprocessor-face in FSF Emacs. - - * generic/proof-compat.el: - Emulate buffer-syntactic-context on FSF Emacs - - * ChangeLog.gz: Updated. - - * twelf/twelf-font.el: - Remove twelf-config-mode variable check, to allow functions - here to work with PG (without loading twelf-old.el). - - * twelf/twelf.el: - Improvements to support: needs work in segment-up-to, though. - -2000-09-18 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-keywords.el: - complete set of keywords from IOA image; - -2000-09-18 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - -2000-09-17 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isa.el: - silent-cmd and init-cmd: activate Isabelle99-1 versions; - - * isar/isar.el: - removed proof-shell-pre-sync-init-cmd (init now handled by -PI options - in isabelle-command-line); - tuned comments; - - * isa/isabelle-system.el: - isabelle-command-line: include -PI options for isar; - activate global-timing; - - * isa/interface: - this file is now a COPY of isar/interface; - - * isar/interface: - -I option for Isar vs. classic Isabelle mode; - tuned; - -2000-09-15 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/interface, isar/interface: - isatool installfonts (for remote X-Symbol fonts); - -2000-09-15 Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> - - * af2/af2-font.el, af2/af2-fun.el, af2/af2.el: - various fixes. - . - - * generic/proof-script.el: - added proof-retract-current-goal - - * generic/proof-script.el: - added proper call to proof-remove-comment before matching with proof-xxx-with-hole-regexp - - * generic/proof-utils.el: - removed some debugging messages I forgot - - * generic/proof-utils.el: - added function string-search and proof-remove-comment - - * af2/af2.el: - major modifications including outline, atgs, ... - - * af2/af2-outline.el: - outline minior mode definitions for af2 - - * af2/af2-font.el: - font-lock and sym-lock definitions for af2 - - * af2/af2-tags.el: - tags functions for af2 - - * af2/af2-fun.el: - usefull function definitions for af2 - -2000-09-14 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - renamed \<brokenbar> to \<bar>; - fixed glyph of \<pounds>; - - * isa/x-symbol-isabelle.el: - x-symbol-isabelle-electric-ignore: "~="; - -2000-09-14 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * doc/PG-adapting.texi: - Encourage use of easy instantiation mechanism. - - * demoisa/demoisa-easy.el: - Encourage use of demoisa-easy.el - - * generic/proof-script.el: - Remove FIXME. - - * generic/proof-config.el: - Improved docstrings, comments. - - * doc/ProofGeneral.texi: - Moved proof-add-completions to adapting manual - - * doc/PG-adapting.texi: - Added doc of completions, several other script settings. Sections in script chapter. - - * doc/PG-adapting.texi: - Note about creating images for toolbar. - - * etc/cvs-tips.txt, CHANGES, README.devel, todo: - Updated - - * html/header.phtml, html/links.phtml, html/main.phtml, html/news.phtml, html/oldrel.phtml, html/register.phtml, html/download.phtml, html/elispmarkup.php3, html/features.phtml, html/about.phtml, html/devel.phtml: - Updates - - * html/images/bullethole.gif: - Shrunk a bit - - * images/notes.txt: Updated. - -2000-09-13 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/todo: - done: make help key bindings appear in "Show me ..." menu; - - * generic/proof-x-symbol.el: - capitalize xs-lang-name; - -2000-09-13 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * doc/PG-adapting.texi: - Removed keystroke index. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README: - Added some bug test cases. - - * CHANGES, todo: - Updated - - * Makefile: - Added af2 and twelf to elisp dirs. - - * etc/release-log.txt: - Getting ready for 3.2 release - - * html/functions.php3, html/gallery.phtml, html/header.phtml, html/develdownload.phtml, html/doc.phtml, html/download.phtml, html/features.phtml: - Minor changes and improvements - - * html/images/pg-text.gif, html/images/ProofGeneral.jpg: - Reduced sizes of images. - - * html/proofgen.css: - Revamp style a bit -- not so good with netscape but OK elsewhere. - - * images/pg-text.gif, images/pg-text.xcf, images/ProofGeneral.gif, images/ProofGeneral.jpg, images/ProofGeneral.xcf: - Reduced sizes of images. - - * doc/PG-adapting.texi: - Remove keystroke index, add appendix with demoisa code (directly included) - - * generic/proof-config.el: - Docstring changes for printed docs. - - * doc/PG-adapting.texi: - Add sections to chapter 2, and text on adjusting toolbar. Update magic - - * af2/af2.el: - Add removal of state button as test example. Replace af2-with-xemacs -> proof-running-on-XEmacs. - - * af2/example.af2: - Add trivial test command. - - * generic/proof-config.el: Order change - - * generic/proof-toolbar.el: - Removed proof-toolbar-entries-default and <PA>-toolbar-entries. - - * doc/PG-adapting.texi, doc/ProofGeneral.texi: - Minor improvements - - * generic/proof-script.el: - Remove ambitious promise to implement proper generic-find-and-forget. - - * generic/proof-config.el, generic/proof-toolbar.el: - Make <PA>-toolbar-entries, and move it and proof-toolbar-entries-default to proof-config to allow easier configuration. - -2000-09-12 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * Makefile.devel: - Make ordinary dist before develdist, because dist clears build dir... whoops. - - * ChangeLog.gz: Updated. - - * etc/cvs-tips.txt: - Notes about using cvs remotely added. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * doc/PG-adapting.texi: Updated magic. - - * doc/docstring-magic.el: - Add provide sym-lock to fix sym lock loading problem - - * doc/PG-adapting.texi: - More details about parsing functions. Improved intro - - * doc/ProofGeneral.texi: Update date. - - * generic/proof-script.el: - Remove shell important setting from script ones. - - * af2/example.af2: - Rather empty example. - - * af2/af2.el: - Add syntax config for block comments, and remove path from af2-prog-name. - - * todo: Updated - - * generic/proof-shell.el: - Add sanity check on important settings for proof shell (underway) - - * generic/proof-site.el: - Added entry for Af2 - - * generic/proof-config.el: - Docs for proof-shell-eager-annotation-start stuff - - * af2/af2.el: - New version sent by Christophe. - -2000-09-11 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - proof-shell-pre-interrupt-hook for PolyML 3 only; - -2000-09-11 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * af2/af2.el, af2/sym-lock.el: - New prover, first bash. - - * generic/proof-config.el, generic/proof-script.el: - Added proof-shell-annotated-prompt-regexp to important settings, removed safe default of empty string (now will have error msgs from filter) - -2000-09-08 David Aspinall <da@proofgeneral.org> - - * doc/ProofGeneral.texi: - Customize always available if PG is - - * todo: Updated - - * isa/isabelle-system.el: - Changes for selecting object logic, locating executables. - - * generic/proof-utils.el: - ADded proof-locate-executable. - - * generic/proof-script.el: - Fix obscure problem with proof-segment-upto-cmdstart with buggy input. - - * generic/proof-config.el: - Rearrangement - -2000-09-07 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-keywords.el: - removed "of", "congs"; - added "hints"; - -2000-09-03 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: - removed unused variable C; - -2000-09-02 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/interface, isa/interface: - more quoting; - -2000-08-30 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: use isar-markup-ml; - eliminated superficial semicolons; - fixed proof-shell-quit-cmd; - -2000-08-29 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - syntax: "?" made word char; - -2000-08-29 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml: - Set version tag for new release. - - * html/news.phtml: Tweak - - * twelf/example.elf: - Example file grabbed from twelf distrib - - * twelf/twelf.el: - A little bit of progress. - - * doc/PG-adapting.texi, generic/proof-config.el, generic/proof-shell.el: - Added proof-shell-auto-terminate-commands - -2000-08-28 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * todo: - adapting manual needs intro fixing - - * doc/ProofGeneral.texi: - Fix description of manual now broken into two - - * doc/PG-adapting.texi: Updated magic - - * doc/Makefile: Fix recursive make - - * etc/cvs-tips.txt: - Note about CVSROOT setting. - - * isa/isabelle-system.el: Branch - - * isa/isabelle-system.el: - Remove Library.timings call, restore compatibility with I99. - - * twelf/twelf.el, twelf/twelf-old.el, twelf/twelf-font.el: - Branch - - * twelf/twelf.el, twelf/twelf-old.el, twelf/twelf-font.el: - Files for twelf, not working at all yet. - - * TODO: Updated - - * todo: Added a couple of todos - - * isar/isar.el: - Change name of mode: isar-proofscript-mode -> isar-mode and remove - alias. Regular mode name needed for fancy macros. - - Use proof-definvisible fancy macro to define help menu functions. - Removed parentheses from menu entries so key bindings show up. - - * doc/ProofGeneral.texi: - Missing full stop - - * etc/isa/settings.ML: - Test file for proof-shell-set-elisp-variable-regexp - - * isa/isa.el: - Added setting for proof-shell-set-elisp-variable-regexp - - * generic/proof-shell.el, generic/proof-config.el: - Added proof-shell-set-elisp-variable-regexp - - * generic/proof-site.el: - Added twelf and experimental support note. - - * generic/proof-menu.el: - FIXME note added, missing docstring from macro fn def. - - * html/news.phtml, html/oldnews.phtml: - News updated - - * html/doc.phtml, html/develdownload.phtml: - Link to two manuals now. - - * doc/README.doc, doc/localdir, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile: - Split manual into two parts. - - Added notes about find theorems trick of separating constants by comma - for Isabelle. Made for version 99-1. - - Improved documentation for urgent messages, including recent - additions. Mentioned new high-level macros proof-defshortcut, - proof-definvisible. - -2000-08-28 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el, isa/isa.el: - cd command: add_path; - - * isa/interface-setup.el: - conditional load of proof-site.el; - - * isar/interface, isa/interface: - -w false implies -x false; - do not load proof-site.el here; - -2000-08-26 Pierre Courtieu <courtieu@lri.fr> - - * coq/x-symbol-coq.el: - nothing important, I forgot to undo something before my last commit in - coq/x-symbol-coq.el - - * coq/x-symbol-coq.el, coq/coq-syntax.el, coq/coq.el: - Some changes for undoing with coq, handle user-defined tactics, in - coq/coq-syntax.el and coq/coq.el. - -2000-08-23 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - more symbols; - - * isa/interface-setup.el: - tuned x-symbol setup; - -2000-08-16 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - isar-keywords-proof-improper; - - * isar/isar-keywords.el: - added isar-keywords-proof-improper; - tuned; - -2000-08-14 David Aspinall <da@proofgeneral.org> - - * generic/proof-depends.el: - Added Fiona's changes, cleaned up a little bit with header and footer - - * generic/proof-shell.el: - Added split string on theorem dependency code, to make list of dependents. - - * generic/proof-script.el: - Added Fiona's changes, cleaned up a little bit - - * isa/thy-mode.el: - Added Fiona's changes. - - * etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy: - Files for testing theorem dependency features. - -2000-08-14 Pierre Courtieu <courtieu@lri.fr> - - * coq/coq.el: - enhancement of outline regexps for coq, now when hiding bodies, we see - completely definitions and theorems, but proof script are hidden (but - can be blindly sent to the prover). Seems to work correctly. - - * coq/x-symbol-coq.el: - enhancement of x-symbol for coq, philosophy is not encoded, and phi1 is, - one problem remains: a word ending with phi will be encoded. - -2000-08-09 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/interface-setup.el: - smart setup of X-Symbol mode; - -2000-08-09 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - -2000-08-07 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - added outline mode setup (still not quite working as expected); - - * isar/isar.el: - cleaned up outline stuff; - - * isar/isar-keywords.el: - new category isar-keywords-proof-heading; - -2000-08-03 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/todo: - ** B make help key bindings appear in "Show me ..." menu; - - * isar/isar.el: - added isar-help functions / keys (how do I get keys into menus?); - - * isa/x-symbol-isabelle.el: - x-symbol-isabelle-electric-ignore: include [[ ]]; - - * generic/proof-script.el: - handle comment inside a command (patch by da); - -2000-08-02 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/x-symbol-isabelle.el: - x-symbol-isabelle-prepare-table: avoids redundancy in code, improves - on isar version (only 1 backslash); - - * isa/Example.ML, isa/Example.thy, isa/Example2.ML: - tuned; - - * isa/isa.el: added isa-preprocessing; - -2000-07-29 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - fixed isar-goals-font-lock-keywords; - - * isar/isar-keywords.el: - added "thm_deps", "overloaded"; - -2000-07-26 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * doc/ProofGeneral.texi: updated; - - * doc/docstring-magic.el: - use proof-assistant-table instead of proof-assistants; - -2000-07-26 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * isa/todo: Suggestion from DvO added - -2000-07-20 David Aspinall <da@proofgeneral.org> - - * etc/test-schedule.txt: - Note about need to test.. - -2000-07-20 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * generic/proof-site.el: - proper evaluation of PROOFGENERAL_ASSISTANTS vs. proof-assistants; - - * generic/proof-easy-config.el: - fixed comment; - -2000-07-20 David Aspinall <da@proofgeneral.org> - - * isa/isa.el: - Remove accidental testing setq left in. - -2000-07-19 David Aspinall <da@proofgeneral.org> - - * COPYING: Fix date - - * generic/proof-shell.el: - bug fixing in matching theorem dependencies - - * generic/proof-depends.el: - functions for manipulating theorem dependencies - - * isa/isa.el, isa/depends.ML: - experiments with theorem dependencies - - * generic/proof-shell.el, generic/proof-script.el, generic/proof-config.el: - changes to add theorem dependencies recording in spans - -2000-07-19 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: - use ML_command to avoid unwanted output; - -2000-07-19 David Aspinall <da@proofgeneral.org> - - * isa/isa.el: reverting to last version - -2000-07-19 fionam <fionam@dcs.ed.ac.uk> - - * isa/depends.ML, isa/isa.el: - file for theorem dependencies - -2000-07-17 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * CHANGES: tuned; - -2000-07-16 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * coq/coq.el: - Removed some (hopefully redundant) requires. - - * html/projects/pgml.html, html/projects/pgip.html: - Modified, now white paper contains DTDs (soon) - - * papers/README: - Note that theres nothing there yet. - -2000-07-13 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml: - Set version tag for new release. - - * etc/ProofGeneral.spec: - Add Isabelle interface scripts to RPM - -2000-07-12 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * CHANGES, todo: - Updated - - * doc/ProofGeneral.texi, html/about.phtml, html/feedback.phtml, html/gallery.phtml, html/proofgen.css, html/screenshot.phtml: - Minor updates - - * generic/proof-autoloads.el: - Update autoloads. - - * generic/proof-splash.el: - Make proof-splash-message autoload. - -2000-07-08 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - isabelle-command-line: try to be smart in ensuring proper Isabelle - command line, avoiding nil under all circumstances; - - * isar/isar.el: - proof-prog-name: use isabelle-command-line; - removed misc junk; - - * isa/isa.el: - proof-prog-name: use isabelle-command-line; - - * isa/interface-setup.el: - do not change isabelle-prog-name here; - be less aggressive in changing x-symbol-enable; - -2000-07-06 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: - tuned help-menu-entries; - -2000-07-05 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * CHANGES: Updated - - * isa/isa.el: - Fix to make back() undoable. - -2000-07-04 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * html/cvsweb.conf, html/cvsweb.cgi: - CVS web script - - * html/proofgen.css: - Changes for CVS web style fixup - - * html/images/.cvsignore, html/images/silverrule.gif: - Ignore file for xvpics put there by gimp - -2000-07-03 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * isa/isabelle-system.el: - Note about trapping errors - - * todo: Updated - -2000-07-03 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - quick-and-dirty t by default; - -2000-07-03 David Aspinall <da@proofgeneral.org> - - * isa/isabelle-system.el: - Patch to cope gracefully with empty list of Isabelle documents. - -2000-07-01 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - activate global-timing; - - * isar/isar.el: improved help menu; - replaced "help" by "welcome"; - - * isar/isar-keywords.el: - removed 'help'; - added 'print_antiquotations', 'print_commands', 'print_trans_rules'; - - * isa/isabelle-system.el: - tuned docs menu; - -2000-06-30 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-keywords.el: - added method_setup; - -2000-06-29 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * isa/isabelle-system.el: - Added quick-and-dirty setting -- we can still argue about the default, 8-) - -2000-06-27 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * generic/span-overlay.el: Minor tweak. - - * todo, TODO: - Updated - - * isar/todo: - Note about typing in shell buffer - - * isar/isar.el, isa/isa.el: - Tidy - - * etc/isar/multiple/C.thy: - Added tag to force Isar mode - -2000-06-26 David Aspinall <da@proofgeneral.org> - - * generic/proof-script.el: - Fix mark buffer atomic problem (caused multiple file oddity with Isar), for new parsing functions. - -2000-06-22 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml: - Set version tag for new release. - - * isa/Example.ML: Added missing proof. - - * isar/Example.thy: Extra note. - - * CHANGES: XEmacs only note - - * FAQ: - Rearranged, more info about X-Sym probs - - * generic/proof-shell.el: - Remove modeline from extra frames (in XEmacs). - - * generic/proof-config.el: - Added back defconsts for face names needed for FSF Emacs. - Yet another annoyance with FSF. - -2000-06-22 Pierre Courtieu <courtieu@lri.fr> - - * coq/coq.el, coq/coq-syntax.el: - somme little changes to make undo work better - -2000-06-19 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * isa/isabelle-system.el: - Fix typo causing missing proof-shell-pre-interrupt-hook. - - * README.devel: Fix typo - - * doc/ProofGeneral.texi: - Updated list of helpers. Typo - -2000-06-16 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el, isar/isar-syntax.el: - proper function-menu (fume) setup; - - * isa/isa.el, isa/isa-syntax.el: - proper indentation setup; - - * isa/Example.ML: proper indentation; - - * generic/proof-script.el: - proof-script-find-next-entity: support list of match items; - replaced spurious re-search-forward by proof-re-search-forward; - proof-script-important-settings: commented out proof-goal-with-hole-regexp, - proof-save-with-hole-regexp; - - * generic/proof-config.el: - proof-script-next-entity-regexps: admit list of MATCHNOS; - -2000-06-16 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * isa/x-symbol-isabelle.el: - Renamed x symbol language name to isabelle (rather big for status line, unfortunately) - - * isa/isa.el, isa/isabelle-system.el, isar/isar.el: - Tuned x-symbol config, moved settings to isabelle-system.el - - * generic/proof-config.el, generic/proof-x-symbol.el: - Added pgcustom x-symbol-language to allow different language name than proof assistant - - * isar/x-symbol-isar.el: Deleted files. - - * isa/x-symbol-isa.el, isa/x-symbol-isabelle.el: - Renamed file - - * CHANGES: - Note about new indentation code and current buggy state - -2000-06-15 David Aspinall <da@proofgeneral.org> - - * todo: - Added new section on updates for future Emacs versions - - * CHANGES: Updated - - * isar/x-symbol-isar.el: Note to merge - - * isa/isa.el: - First attempt at using new indentation for Isabelle. Utterly broken. - - * generic/proof-toolbar.el: - Support toolbar in gtk-xemacs - - * generic/proof-x-symbol.el: - More comments at top of file - - * README: Web addr note - - * generic/proof-config.el: - Improved some docstrings. - Simplified face configuration by using auxiliary macro. - Now also works for gtk-xemacs. - Experimented with removing spurious face alias constants. - - * doc/ProofGeneral.texi: - Elaborated on where to find example file - -2000-06-10 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/todo: new indentation setup; - -2000-06-09 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * INSTALL, todo: - Message about packages needed (incomplete) - - * plastic/plastic.el: - Removed spurious requires. - - * doc/ProofGeneral.texi: Updated magic. - - * doc/docstring-magic.el: - Load a couple more file manually. - - * generic/proof-shell.el: - Strange ? got in by accident. - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * generic/proof-script.el: Comment - - * CHANGES, generic/proof-shell.el: - Remove toolbar and menubar from windows in multiple frame mode. - - * todo: Bug in file colouring - -2000-06-09 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - fixed show_sorts; - - * isar/isar.el: - proof-shell-error-regexp; - -2000-06-08 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: new indentation setup; - completion-table: use isar-keywords-major; - - * isar/isar-syntax.el: - new indentation setup; - - * isar/isar-keywords.el: - isar-keywords-proof-open/close; - - * isar/Example.thy: proper indentation; - - * plastic/plastic.el, isa/isa.el: - adapted to new indentation setup; - - * generic/proof-indent.el: - rewrote code from scratch: faster, easier to configure; now enabled by default; - - * generic/proof-config.el: - settings for new indentation setup; - - * generic/proof-syntax.el: - added proof-looking-at-safe, proof-looking-at-syntactic-context; - removed proof-indent-commands-regexp; - - * doc/ProofGeneral.texi: - completely new indentation setup: faster, easier to configure; - now enabled by default; - - * lego/lego.el: - basic setup for new indentation code; - - * coq/example.v: proper indentation; - - * coq/coq.el: - basic setup for new indentation code; - - * todo: - Improved indentation code; enabled by default; - -2000-06-07 David Aspinall <da@proofgeneral.org> - - * isar/isar.el: - Failed attempted hack to support ML files in isar mode (see comments in isar-preprocessing). - - * isa/isa.el: - Removed disable of simp tracing from enable/disable pr, desired functionality now in Isabelle's update_thy for PG - -2000-06-06 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml: - Set version tag for new release. - - * todo: todo for C-c C-l to fix point - - * Makefile.devel: - Make distclean rather than clean do the CVS pruning. - - * generic/proof-script.el: - Added special hack for Isar to include proof-terminal-char in sent string. - - * isar/isar.el: - Allowed ; to terminate a command by including it in regexp for cmdstart - Added completion for Isar keywords and X-symbol token names. - -2000-06-05 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - isar-save-with-hole-regexp: proof-no-regexp; - - * isar/isar.el: - proof-indent-commands-regexp: use proof-no-regexp; - isar-global-save-command-p: more robust wrt. empty prev span (malformed!?); - isar-preprocessing: fixed terminator regexp; - - * isa/isabelle-system.el: - improved isabelle-verbatim-regexp: use \` \' instead of ^ $; - - * generic/proof-syntax.el: - fixed proof-anchor-regexp: use \` instead of ^; - added proof-no-regexp; - -2000-06-05 David Aspinall <da@proofgeneral.org> - - * isar/isar-syntax.el: - Removed defunct comments - - * isar/isar.el: - Temporary bug fix to solve nil span error message - - * todo: Updated. - - * CHANGES: - proof-next-error, proof-display-some-buffers - - * doc/ProofGeneral.texi: - Added paragraph and index entry explaining prefix arguments, - and some more on keystrokes, for the Emacs-impoverished users. - Added doc of proof-display-some-buffers - - * isa/thy-mode.el: - Added proof-next-error to menu. - - * isa/isa.el: - Added settings for proof-next-error. - Added switch off of simplifier tracing to quiet command - (not good enough -- need help from Isabelle for that really). - - * generic/proof-menu.el: - Added miscellaneous commands section, with proof-display-some-buffers - function. - Bind C-c C-l to proof-display-some-buffers, add to buffer menu. - Move start/exit to proof assistant specific menu. - Added proof-next-error to menu. - - * generic/proof-utils.el: - proof-clean-buffer: clear next error flag if buffer is response. - - * generic/proof-config.el: - Tweaked some docstrings. - Added proof-shell-next-error-regexp and friends. - Bind proof-shell-next-error in proof-universal-keys. - - * generic/proof-shell.el: - Added proof-next-error. - proof-shell-invisible-command: add terminator if it seems to be - missing (after all: it's useful for users with C-c C-v). - - * generic/proof-autoloads.el: - Updated to add proof-next-error. - -2000-06-05 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isa-syntax.el: - fixed output syntax table; - -2000-06-04 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * generic/proof-script.el: - proof-segment-up-to-cmdstart/end: use proof-re-search, proof-looking-at! - - * generic/proof-syntax.el: - proof-re-search-forward/backward: observe proof-case-fold-search; - - * isa/isa-syntax.el: - replaced isa-verbatim by isabelle-verbatim; - - * isa/isabelle-system.el: - added isabelle-verbatim; - fixed proof-shell-pre-interrupt-hook: use isabelle-verbatim; - - * isar/isar.el: - replaced isar-verbatim by isabelle-verbatim; - added isar-strip-terminators; - - * isar/todo: updated; - - * isar/isar-syntax.el: - replaced isar-verbatim by isabelle-verbatim; - fixed output syntax table; - - * generic/proof-script.el: - proof-segment-up-to-cmdstart: exclude leading blanks from command string; - -2000-06-03 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * generic/proof-script.el: - improved proof-segment-up-to-cmdstart: handle overlap of command - prefix and comment/string (e.g. { vs {* in Isar); - - * isar/isar-keywords.el: { } are back; - -2000-06-02 Pierre Courtieu <courtieu@lri.fr> - - * coq/coq.el: - Added 3 entries in the Coq menu: Print Check and Hints - -2000-06-01 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * generic/proof-autoloads.el: Updated - - * generic/proof-menu.el: Added autoload - - * html/develdownload.phtml: - Added links to latest manual - - * etc/isar/Parsing.thy: - File used to test new parsing mechanism. - - * etc/pgkit/xmltest2.xml, etc/pgkit/xmltest1.xml: - New test files for PG kit. - - * doc/ProofGeneral.texi: - Added proof-comment-{start,end}-regexp. - Added proof-segment-up-to-{cmdstart,cmdend} and details of - which is selected. - Updated magic. - - * todo: Updated - - * todo: - Note about generalizing settings mechanism - - * coq/coq.el: - Removed time setting, added proof-assistant-settings-cmd to init string, but commented out - - * coq/coq.el: - Added a couple of settings for Coq - - * generic/proof-menu.el: - Allow two strings for boolean settings to handle non-uniformity in Coq - - * generic/proof-config.el, generic/proof-shell.el: - Use proof-running-on-XEmacs variable. - - * generic/proof-script.el: - Use proof-running-on-XEmacs variable. Don't set proof-segment-up-to alias if already set. - - * BUGS: Plea for debugging in FSF Emacs - - * CHANGES: - Updated, mentioning new parsing function mechanisms - - * isa/Example-Xsym.ML: - Remove spurious spaces - - * isar/Example.thy: - Removed now spurious semicolons, 8-). - - * isar/isar-keywords.el: - Temporarily removed keywords { and } for new parsing mechanism - - * isar/isar.el: - Remove setting of proof-segment-up-to - - * generic/pg-xml.el: New file - - * generic/proof-script.el: - New parsing functions proof-segment-up-to-cmd{start,end} - Select new parsing function according to config variables - Use proof-comment-{start,end}-regexp, and set default values - in proof-config-done-related, from proof-comment-{start,end} - New proof-script-complete which uses proof-case-fold-search - - * generic/proof-menu.el: - Changed 'complete to 'proof-script-complete to use proof-case-fold-search. - - * generic/proof-shell.el: - Made require on proof-menu instead of proof-script. - - * generic/proof-indent.el: - Use proof-comment-{start,end}-regexp - - * generic/proof-config.el: - Added proof-comment-start-regexp, proof-commend-end-regexp. - Mention proof-script-complete in docstring for proof-case-fold-search. - - * lego/lego.el: - Remove spurious requires. - -2000-05-31 David Aspinall <da@proofgeneral.org> - - * isa/isabelle-system.el: - Commented out global-timing since it seems to be Isabelle99-1 specific. - - * isa/isa.el: - Added old completion table from Isamode. Added code to automatically add completion for x-symbol tokens. - - * generic/proof-menu.el: - Fix keybinding for completion. Add completion to menubar. - - * generic/proof-compat.el: - Added hack to completion.el to avoid adding every prefix as completion. - - * generic/proof-x-symbol.el: - Compatibility with completion package. - - * generic/proof-script.el: - Fixes for completion support. - -2000-05-30 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - improved isar-goals-font-lock-keywords; - -2000-05-30 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml: - Set version tag for new release. - - * isa/isa.el: - Added missing command terminators for proof-xsym commands - - * generic/proof-script.el: - Hairy parsing for Isar. Not finished (or working) yet. - - * generic/proof-script.el: - Arg for proof-minibuffer-cmd: compact whitespace in region. - - * generic/proof-script.el: - Fixed typo causing bug. Generic parsing updated (still wip) - -2000-05-30 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/interface-setup.el: - handle 'isa-x-symbol-enable vs. 'isar-x-symbol-enable; - -2000-05-30 David Aspinall <da@proofgeneral.org> - - * isar/isar.el: - isar-preprocessing inserts final terminator if none there. - Added (defpgdefault script-indent t) to turn on indentation. - Added proof-script-command-start-regexp setting. - - * generic/proof-shell.el: - Change order of checks in proof-shell-live-buffer - -2000-05-30 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - defpacustom global-timing; - -2000-05-30 David Aspinall <da@proofgeneral.org> - - * generic/proof-compat.el: - Added process-live-p - - * generic/proof-config.el: - Added proof-script-command-start-regexp. Updated docstrings to reflect that proof-terminal-char no longer appended to commands. - - * generic/proof-indent.el: Tidied - - * generic/proof-script.el: - Added doc of new prefix arg feature for proof-minibuffer-cmd - - * generic/proof-script.el: - Added prefix arg to proof-minibuffer-cmd to insert current region. - -2000-05-29 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * CHANGES: - Favourites mechanism now fully implemented, I hope. - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * isa/isa-syntax.el: Docstring - - * isar/isar-syntax.el: - Tweak font lock exprs enough for Example.thy - - * isar/isar-syntax.el: - Font lock exprs for goals buffer like those in Isabelle - - * isar/isar.el: - Set settings format function before calculating initial command. Add hilit for goals buffer - - * isa/isabelle-system.el: - Remove isar-markup-ml from here - - * isar/isar.el: - Use generic default setting mechanism now. Add isar-markup-ml here. - - * isar/Example.thy: - Add -*- isar -*- tag to force mode, and comment to explain. - - * CHANGES: Updated - - * generic/proof-script.el: - Added new parsing mechanism. Began removing proof-terminal-string. - - * coq/coq.el, lego/lego.el: - Removed use of proof-terminal-string, added explicit terminators everywhere. - - * todo: Updated - - * etc/announce: - Updated for announcement. - - * doc/ProofGeneral.texi: - Updated with new keybindings for Coq, Lego. - - * lego/lego.el: - Changed keybindings for lego specific functions - - * coq/coq.el: - Changed keybindings for coq specific functions - - * isa/isabelle-system.el: - Generalized proof assistant settings mechanism - - * isa/isa.el: - Add explicit terminators to commands. Generalized isabelle-set-default-cmd. - - * isa/isa-syntax.el: - Additions to font lock on output - - * generic/proof-autoloads.el: Updated - - * generic/proof-shell.el: - Don\'t wait for ever if process dies on startup - - * generic/proof-syntax.el: - Generalized proof-format to allow sexps in replacement. - - * generic/proof-indent.el: - Missing parenthesis - - * generic/proof-utils.el: - Added functions for defining string and integer setters, for proof assistant settings. - - * generic/proof-menu.el: - New stuff for making proof assistant settings. - - * generic/proof-config.el: - Added configuration variables for proof assistant settings. Docstring for favourites. - - * generic/proof-compat.el: - Added replace-string for FSF. - - * plastic/plastic.el: - Fixed define-key calls. Set useful default for plastic prog name - -2000-05-26 David Aspinall <da@proofgeneral.org> - - * generic/proof-syntax.el: Docstring. - - * lego/lego.el, isa/isabelle-system.el, coq/coq.el: - proof-defass-default -> defpgdefault - - * generic/proof-script.el: - Removed proof-script-indent check. - - * generic/proof-indent.el: - Update to use generic option indent-line, and switch inside - function rather than mode (so can be turned on/off easily). - - * generic/proof-x-symbol.el: - Switch to using per-prover generic option for x-symbol-enable. - - * generic/proof-menu.el: - Binding for complete. - Proper toggler use for generic option x symbol enable. - - * generic/proof-utils.el: - Macros for generic custom settings from proof-config. - Made proof-set-value work with generic settings as well as global ones, - hacking a name for a generic function. - - * generic/proof-config.el: - Rename proof-defass-custom -> defpgcustom. - Moved macros for generic custom settings to proof-utils. - Made proof-x-symbol-enable be generic (isa-x-symbol-enable, etc). - Ditto proof-script-indent. - Added proof-shell-pre-sync-init-cmd - Added PA-completion-table, PA-tags-program. - -2000-05-26 Paul Callaghan <P.C.Callaghan@durham.ac.uk> - - * plastic/plastic.el, plastic/test.lf: - fixed error in test.lf - - fixed conflict in plastic.el - -2000-05-26 David Aspinall <da@proofgeneral.org> - - * generic/proof-compat.el: - Moved compatibility code into proof-compat.el - - * generic/proof-site.el: - Only extend the load path if necessary - - * Makefile.xemacs: - Comments, still nothing here. - - * Makefile: - Clean also deletes CVS temporaries (naughty, should be in devel.clean really) - - * todo: Updated - - * doc/ProofGeneral.texi: Updated magic - - * generic/texi-docstring-magic.el: - Attempt to quote @ (failed, dunno why) - -2000-05-26 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el: - isar-any-command-regexp; - - * isar/isar-keywords.el: - isar-keywords-major; - -2000-05-25 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * generic/proof-config.el: - Temp hacks to get doc to build before proper commits. - - * generic/proof-config.el: - Made x-symbol-enable be individual option. - - * generic/proof-script.el: - Added completion table code. - - * doc/docstring-magic.el: - Fixes for PA docs, and file load order. - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.patch: - Patched patch again. - Phew, what an effort. - - * coq/coqtags: - Spurious newline causing patch to fall over. - - * isar/isar.el: - Removed spurious code in isar-mode function. - Removed defunct key binding of C-c C-l (Overriden with goto-end-of-locked). - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec: - Fix applying of patch. - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.patch: Fix patch. - - * etc/ProofGeneral.patch: - Updated patch. - - * ChangeLog.gz: Updated. - - * coq/coqtags, lego/legotags: - Revert to previous path for perl, better default for non-linux. Linux uses RPM, where its fixed. - - * ChangeLog.gz: Updated. - - * doc/ProofGeneral.texi: Fix info bug. - - * ChangeLog.gz: Updated. - - * html/doc.phtml, Makefile.devel: - Make doc link to 3.1, not pre-release. Minor extra editing on new release. - - * doc/ProofGeneral.texi: - Doc more new features and bug fixes for 3.2. - Doc new PA-<name> mechanism. - Doc for completion. - Doc for proof-shell-pre-sync-init-cmd. - - * CHANGES: - Note about proof-shell-pre-sync-init-cmd - - * BUGS: - Note about fix for C-x C-f and friends - - * etc/bug-notes.txt: - Note about sync problem - - * lego/lego.el, isa/isa.el, isar/isar.el, generic/proof-shell.el, generic/proof-config.el: - Patch for synchronization problem in Coq, perhaps others. - - * etc/README, etc/bug-notes.txt: - New file, test cases for bugs - - * Makefile: - Add target for editing perl scripts too - - * coq/coqtags, lego/legotags: - Change default path to perl - - * ChangeLog.gz: Updated. - - * html/news.phtml: - Second toolbar patch in 3.1.6 now. - - * etc/release-log.txt: - Updated from 3.1 branch - - * generic/proof-toolbar.el: - When button enablers disabled, don't use itimer or after-change hook. - - * ChangeLog: Updated. - - * etc/release-log.txt: - Second toolbar patch. - - * generic/proof-toolbar.el: - When button enablers disabled, don't use itimer or after-change hook. - - * ChangeLog.gz: Updated. - - * CHANGES: Toolbar fixes. - - * generic/proof-toolbar.el: - Next button is enabled whenever locked region is not full. - - * ChangeLog.gz: Updated. - - * html/develdownload.phtml: Minor - - * etc/ProofGeneral.spec, generic/proof-site.el, html/devel.phtml, html/develdownload.phtml: - Set version tag for new release. - - * html/links.phtml: Added link to HELM - - * html/news.phtml: Fix para spacing - - * html/news.phtml: Note about 3.1.6 - - * ChangeLog: Updated. - - * generic/proof-site.el: - Set version tag for new release. - - * generic/proof-config.el, etc/release-log.txt, doc/ProofGeneral.texi: - Turn off button enablers when running on Solaris - -2000-05-24 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-keywords.el: added "done"; - -2000-05-22 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el, isar/isar-syntax.el: - replaced proof-ids-to-regexp by isar-ids-to-regexp, which admits - keywords to consist of a single non-word char as well (e.g. { }); - - * isar/isar-keywords.el: - replaced {{ }} by { }; - -2000-05-19 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-syntax.el, isar/isar.el: - isar-verbatim-regexp: include \n; - -2000-05-18 David Aspinall <da@proofgeneral.org> - - * todo: - Updated. Noted that "first line" bug is more prevalent than thought. - -2000-05-18 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isa.el: - Goals.enable/disable_pr: improved version for Isabelle99-1 (commented out); - -2000-05-17 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * generic/proof-menu.el: - Clarify favourites command: key sequence will begin with C-c C-a. - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * html/papers/pgtalk.pdf: Updated - -2000-05-17 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isabelle-system.el: - added show-consts, long-names; - improved isar-markup-ml; - - * isar/isar.el, isar/interface, isar/interface-setup.el: - re-use isa/interface-setup.el rather than separate isar version; - -2000-05-16 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - -2000-05-16 Pierre Courtieu <courtieu@lri.fr> - - * coq/coq.el: - debugging coq menu for old Xemacs compatibility, David said he will do this - for other provers (already done ?). - -2000-05-16 David Aspinall <da@proofgeneral.org> - - * lego/lego.el: - Fix buttons must be 3 long error (for 20.4 compatibility) - - * ChangeLog.gz: Updated. - - * html/doc.phtml: Reference tweak - - * generic/proof-menu.el: - Fix buttons must be 3 long error - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * generic/proof-utils.el: Docstring fix - - * generic/proof-menu.el: - Fixes for defining favourites, added warning for pre-release users. - - * doc/ProofGeneral.texi: - Updated magic, new funcs. - - * doc/docstring-magic.el: - Fixed to load all files and define proof ass specifc vars. - - * generic/proof-site.el: - Added proof-ready-for-assistant function to help docstring magic. - - * FAQ: Added question asked by Larry. - - * generic/proof-site.el: Comment added - - * generic/proof-script.el: - Add proof-strict-state-preserving setting - - * isa/interface-setup.el, isa/isabelle-system.el, isar/interface-setup.el: - Move setting of proof-shell-pre-interrupt-hook to isabelle-system.el - - * isa/isabelle-system.el: Missing quote - - * generic/proof-config.el: - Added version string to splash. Added proof-strict-state-preserving - - * todo: - Updated, mentioned Solaris bug reported by Markus. - - * html/papers/pgtalk.pdf: - Updated PG talk slides - - * html/doc.phtml: - Better reference to TACAS paper. Added link to white paper draft. - - * Makefile: - Be more generous if bash is not found. - - * Makefile: - Added scripts target to edit Isabelle scripts, patch from Mike Squire. - -2000-05-12 David Aspinall <da@proofgeneral.org> - - * doc/docstring-magic.el, todo: - Notes about fixing docstring-magic. - - * todo: Updated - - * isa/isabelle-system.el: - Fixup menus a bit. Remove proof-prf on options change. - - * isa/isa.el: - Remove proof-assistant-menu-entries, done generically now. - - * isar/isar.el: - Modification of proof-shell-init-cmd. Markus, please help... - - * lego/lego.el: - Remove proof-assistant-menu-entries, done generically now. - - * generic/proof-config.el: - Added proof-defassfun. Comments - - * generic/proof-menu.el: - Use (proof-ass X) instead of function call. - - * isa/isabelle-system.el: - Several name changes isa- -> isabelle-, and made generic for Isar - - * isa/isa.el: Comments - - * CHANGES, generic/proof-menu.el: - Specific keys begin C-c C-a, not C-c a. - - * generic/proof-menu.el, generic/proof-utils.el: - Moved utility functions to proof-utils. - - * isa/isabelle-system.el: - Fix to menu definition. - - * generic/proof-config.el: - Fix to function name - - * lego/lego.el: Fix note. - -2000-05-11 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * hol98/example.sml: - Explanatory comments - - * lego/lego.el: - Changes and compatibility fixes for specific menu/keybindings. - - * isar/isar.el: - Load isabelle-system file shared with Isabelle Proof General. - Add default settings to proof-shell-init-cmd. - Add Isabelle menu to menubar. - - * isa/isabelle-system.el: - Generic help menu for Isabelle and Isabelle/Isar added. - Generalized option settings mechanism. - Added simplifier tracing flag. - - * isa/isa.el: - Moved generic settings to isabelle-system.el. isa-set-default-cmd->isabelle-set.. - - * coq/coq.el: - Changes and compatibility fixes for specific menu/keybindings. - - * CHANGES: Updated - - * html/devel.phtml: Tidied page a bit - - * generic/proof-shell.el: - Note abut ;;;###autoload not working for define-derived-mode. - - * generic/proof-script.el: - Use proof-deftoggle macro. - Comments about failure for ;;;###autoload cookie for define-derived-mode - Attempted fixes for C-x C-w, C-x C-v, revert-buffer. - - * generic/proof-utils.el: - Compatibility hack - - * generic/proof-toolbar.el: - Use proof-deftoggle macro. - - * generic/proof-site.el: - Fix for funnily named provers (Isabelle/Isar) and Emacs compatibility. - - * generic/proof.el: - Extra arg to proof-splash-display-screen. - - * generic/proof-menu.el: - Menus and code cleanup - - * generic/proof-config.el: - Removed duplicate declaration - - * generic/proof-splash.el: - Extra arg to proof-splash-display-screen to serve as an About box. - - * generic/proof-config.el: - New mechanism for defining customization variables per-prover. - - * FAQ: X-Symbol funny chars question - - * etc/test-schedule.txt: Fixup branch - - * etc/test-schedule.txt: New file - -2000-05-09 David Aspinall <da@proofgeneral.org> - - * ChangeLog.gz: Updated. - - * README.devel: Updated - - * html/news.phtml, html/devel.phtml: - Added browsable CVS. - - * isa/todo: - Note about desirable additions to Isabelle - - * isa/Example.ML: New goal. - - * generic/proof-config.el: - New setting on the way... - - * FAQ: - Added question about saving options - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * CHANGES: Updated - - * generic/proof-menu.el, generic/proof-config.el: - Fixup menus. - - * generic/proof.el, generic/proof-site.el, generic/proof-autoloads.el, generic/proof-menu.el, generic/proof-script.el: - Fixup loading. - - * isa/Example-Xsym.ML: New file - - * html/projects/xmlpgip.html: - New project (unlinked yet) - - * generic/proof-script.el: - Removed menus, keybinding. Removed compatibility hacks. Improved loading. - - * generic/proof-shell.el: - Improved loading - - * generic/proof-config.el: - Prevent proof-set-value until proof-config-loaded. (C) on splash screen. - - * generic/texi-docstring-magic.el: - Improved loading - - * generic/span-extent.el, generic/span-overlay.el: - Comments. - - * generic/proof.el: - Removed autoloads, util functions. - - * generic/proof-x-symbol.el: - Improved loading - - * generic/proof-utils.el: - Added some functions for developers. - - * generic/proof-toolbar.el: - Improved loading - - * generic/proof-system.el: Fixup branch - - * generic/proof-system.el: - Moved code to proof-menu.el - - * generic/proof-syntax.el: - Added proof-splice-separator. - - * generic/proof-splash.el: - Splash screen now shown from autoloaded function. - - * generic/proof-site.el: - Remove use of cl. Add require on proof-autoloads. - - * generic/proof-easy-config.el, generic/proof-indent.el: - Improve loading - - * generic/span.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/proof-menu.el: - Fixup branch - - * generic/span.el, generic/proof-autoloads.el, generic/proof-menu.el, generic/proof-compat.el: - New files - - * etc/cvs-tips.txt: Trivial. - - * doc/ProofGeneral.texi: - Updated 3.2 changes - - * Makefile.devel: - Added autoloads target. - - * Makefile: EMACS -> BATCHEMACS var - - * ChangeLog: Updated. - - * etc/release-log.txt, isa/isa.el: - Merged from 3.1.5 - - * etc/release-log.txt: Updated - - * generic/proof-site.el: - Set version tag for new release. - - * isa/isa.el: - Generalized thms_containing - - * doc/Makefile: Added default target - -2000-05-07 David Aspinall <da@proofgeneral.org> - - * generic/proof-config.el: Comments - -2000-05-05 David Aspinall <da@proofgeneral.org> - - * isa/isa.el: Comment. - - * doc/ProofGeneral.texi: - Updated 3.2 details. Keybindings for Coq, LEGO shortcuts changed. - - * ChangeLog.gz: Updated. - - * html/news.phtml: Missing para - - * html/news.phtml: Buglet in html - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * doc/ProofGeneral.texi: - Fix markup bug. - - * doc/ProofGeneral.texi: - Expanded explanation of selecting Isar. - - * todo: Updated - - * Makefile: - make clean removes Emacs backups. Probably safe... - - * html/news.phtml: Hot news about FAQ. - - * CHANGES: Updated - - * isa/isa.el, isa/isabelle-system.el: - isa-system.el -> isabelle-system.el - - * isa/isa-system.el, isa/isabelle-system.el: - Renamed file - - * isa/thy-mode.el: Expanded menu - - * generic/proof-script.el: - Comments. Minor improvements for electric terminator and proof-follow-mode='ignore - - * generic/proof-shell.el: - Corrected header. - - * generic/proof.el: - Moved code into proof-system and proof-utils. - - * generic/proof-system.el: - Files for interfacing with proof system, e.g. maintaining settings. - - * generic/proof-utils.el: - General utility functions, moved from proof.el - - * generic/proof-toolbar.el: - Added menu entry for proof-goto-end-of-locked. - - * generic/proof-site.el: - Added variables for customization groups so they can be set automatically. - - * generic/proof-config.el: - Improved docs, declaration of variables set in proof-site, settings mechanism begun. - - * isa/isa.el: - New code in isa-system.el. - - * isa/isa-system.el: - New file for interfacing with Isabelle system. - - * isa/isa.el, isar/isar.el: - Default to isa-mode or isar-mode according to first one invoked. - - * FAQ: Beginnings of a FAQ. - -2000-05-02 David Aspinall <da@proofgeneral.org> - - * plastic/plastic.el, isa/Example.ML, lego/example.l, lego/lego.el, generic/proof-syntax.el, generic/proof.el, generic/proof-config.el, generic/proof-script.el, CHANGES, coq/coq.el: - Added proof-assistant-keymap and commands for defining insert keys. - -2000-05-01 David Aspinall <da@proofgeneral.org> - - * CHANGES: Cease mentioning plastic. - - * ChangeLog.gz: Updated. - - * generic/proof.el: Helper macros. - - * lego/lego.el: - Added specific menu for LEGO. - - * ChangeLog.gz: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * isa/isa.el: - Added specific menu for Isabelle (early version) - - * coq/coq.el: - Added specific menu for Coq. - - * CHANGES, doc/ProofGeneral.texi, generic/proof-config.el, generic/proof-script.el: - Added proof-assistant-menu-entries for proof assistant specific menus. - - * html/develdownload.phtml: Trivial - - * BUGS, todo: - Added note about new FSF bug discovered, sigh... - -2000-04-28 David Aspinall <da@proofgeneral.org> - - * Makefile.devel: Force in .gz target. - - * ChangeLog.gz: Updated. - - * Makefile.devel: - Keep ChangeLog gzipped. Small saving on repo size. - - * ChangeLog, ChangeLog.gz: - Renamed/gzipped file. - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * etc/cvs-tips.txt: - Note about conflict in merging - - * html/news.phtml, etc/release-log.txt: - Added note about 3.1.4 patch, merged from 3.1 branch - - * etc/README, etc/cvs-tips.txt: - Notes about using cvs and branch. - - * Makefile.devel: - Added warning about releasing from old branch. - - * ChangeLog: Updated. - - * html/news.phtml, etc/release-log.txt: - Note about 3.1.4 release - - * ChangeLog: Updated. - - * generic/proof-site.el: - Set version tag for new release. - - * isa/isa.el, generic/proof-syntax.el: - Apply patch sent by Mike Squire - -2000-04-26 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - -2000-04-25 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: - isar-indent regexps moved to isar-syntax.el; - tuned comments; - - * isar/isar-syntax.el: - removed unused isar-ids; - added isar-indent regexps (from isar.el); - - * isar/isar-keywords.el: - removed "simpset" minor keyword; - -2000-04-25 David Aspinall <da@proofgeneral.org> - - * html/main.phtml: - 20.X -> recent, since XEmacs now on 21. - - * generic/proof-syntax.el: - Fix %r modifier in proof-format-filename. - - * isa/isa.el: - Revert to indended fix for isa-retract-thy-file. - - * CHANGES, generic/proof-script.el: - Note about efficiency/bug fix by Markus. - -2000-04-17 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isa/isa.el: - fixed isa-retract-thy-file: pass theory name only; - fixed some comments; - - * isar/isar-keywords.el: added 'hide'; - -2000-04-15 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * generic/proof-script.el: - proof-segment-up-to: no longer poke around in make-string buffer (now - more efficient, also works around crash bug in xemacs-21.1.7/SuSE); - -2000-04-12 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar.el: - fixed proof-mode-for-goals; - -2000-04-07 David Aspinall <da@proofgeneral.org> - - * lego/readonly/readonly.l: - Fix version. - - * ChangeLog: Updated. - - * Makefile.devel: - Change order in release to make ChangeLog be updated before dist built. - - * ChangeLog: Updated. - - * doc/ProofGeneral.texi: - mode-for-pbp -> mode-for-goals - - * etc/ProofGeneral.spec, html/devel.phtml, html/develdownload.phtml, generic/proof-site.el: - Set version tag for new release. - - * generic/proof-shell.el: Comment. - - * todo: Updated - - * generic/proof-script.el: - More generic message to avoid confusion with Coq searching. - - * generic/proof-config.el: - Generalisation of proof-info-command to string or fn. - - * lego/readonly/readonly.l: - Moved from wrong place. - - * generic/pbp.el: Removed this. - - * todo, CHANGES: - Updated - - * generic/proof-x-symbol.el, generic/proof-shell.el, generic/proof-easy-config.el: - pbp-mode -> goals-mode - - * generic/proof-config.el: - Comments. pbp-mode -> goals-mode - - * isa/isa.el: - Tweak to disable_pr function to allow for it being called twice (why?). - - * plastic/plastic.el: - pbp-mode -> goals-mode - - * hol98/hol98.el: Decoration tweaks - - * demoisa/demoisa.el, isar/isar.el, isa/isa.el, coq/coq.el: - pbp-mode -> goals-mode - - * coq/coq-syntax.el: More decoration - - * lego/lego.el: goals-mode -> pbp-mode - - * lego/lego-syntax.el: - Extra decoration. - - * doc/ProofGeneral.texi: - Updates for 3.2. Added documentation of silent settings. - - * plastic/plastic.el, generic/proof-shell.el, generic/proof-config.el, demoisa/demoisa-easy.el, demoisa/demoisa.el, lego/lego.el, coq/coq.el, hol98/hol98.el, isa/BUGS, isa/isa.el, todo, CHANGES: - Fixed up proof-shell-proof-completed mess nicely. - -2000-04-06 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/x-symbol-isar.el, isa/x-symbol-isa.el: - tuned \<bottom>; - added \<lbrace>, \<rbrace>, \<top>; - -2000-04-05 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/todo, isa/todo: - tuned todo stuff; - - * isar/isar.el, isa/isa.el: - improved print_mode switch; - - * isar/isar-keywords.el: - 'welcome' made diagnostic; - - * isar/isar-keywords.el: - eliminated 'as' keyword; - -2000-04-04 Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - - * isar/isar-keywords.el: - added 'print_claset', 'print_simpset'; - -2000-04-04 David Aspinall <da@proofgeneral.org> - - * ChangeLog: Updated. - - * isa/isa.el: - Added provisional commands for enabling/disabling printing. - - * ChangeLog: Updated. - - * etc/ProofGeneral.spec, html/devel.phtml, generic/proof-site.el, html/develdownload.phtml: - Set version tag for new release. - - * todo: Updated - - * isa/Example2.ML: - Save as Example.ML, except using X-Symbol input tokens. - - * CHANGES: Note of 3.2 changes - - * generic/proof-script.el: - Improved behaviour of electric terminator. - - * todo: Updated - - * generic/proof-shell.el: - Added implementation of silent switch for turning on/off prover output. - - * generic/proof-shell.el: - Added proof-shell-clear-state function to collect together state clearing ops. - - * html/devel.phtml, CHANGES: - Updates for 3.2 series. - - * html/projects/reelcase.html, html/projects.phtml: - Added new project B4 - - * ChangeLog: Updated. - - * generic/proof-site.el: - Set version tag for new release. - - * html/oldnews.phtml, html/news.phtml: - Updated news about 3.1.3, split old news out. - - * etc/release-log.txt: - Note about 3.1.3 release - - * isa/isa.el: - Fix accidently introduced bug with passing full paths to theory loader. - - * generic/proof-syntax.el: - Altered proof-format-filename to add %e and %r specifiers. - - * generic/proof.el, generic/proof-splash.el, generic/proof-script.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-shell.el: - Update copyright dates, comments. - |