2001-09-02 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-08-31 Markus Wenzel * isa/interface, isar/interface: handle relative heap paths gracefully; * isar/isar-keywords.el: back to *official* Isabelle99-2 (later Isabelle dists will provide their own copy of this file); 2001-08-31 David Aspinall * CHANGES: Improved explanation * doc/ProofGeneral.texi: Something about dependencies feature * CHANGES: Added note about dependency feature. * generic/proof-depends.el: (Almost) complete rewrite * generic/proof-autoloads.el: Updated * generic/proof-script.el: Move theorem dependency code into proof-depends.el. Added 'controlspan property to proof body spans: action will be controlled from the control span. (The 'goalsave is the parent). Replace 'highlight face with 'proof-mouse-highlight-face throughout. * generic/pg-user.el: Added copy command, call to dependency menu if proof-depends is loaded. * isa/depends.ML: Add simulations of more qed commands, also sort and uniquify dependencies. * generic/proof-config.el: Add new proof-mouse-highlight-face to use instead of default. Fix dependency faces. 2001-08-31 Markus Wenzel * isar/isar-keywords.el: new commands (proof terms, code generator); 2001-08-31 David Aspinall * ChangeLog: Remove duplicate entries * generic/proof-config.el: Add faces for theorem dependencies. * etc/coq/multiple/README: Explanation * AUTHORS: Add DvO to list * AUTHORS: Add Christophe to list * coq/coq.el: Add auto-compile-vos experimental setting for automatic multiple files. * BUGS: Remove minibuffer bug * isa/thy-mode.el: Fix for names of functions in proof-depends * isa/isa.el: Add setting for turning on theorem dependency tracking * isa/depends.ML: Update for Isabelle99-2 * generic/proof-depends.el, generic/proof-script.el: Clean up of proof-depends * generic/proof-menu.el: Skip settings which have no PA command in proof-assistant-settings-cmd * generic/proof-shell.el: Add proof-shell-kill-function-hooks 2001-08-30 Markus Wenzel * isa/interface, isar/interface: include ISABELLE_HOME_USER/etc/isar-keywords.el or ISABELLE_HOME/etc/isar-keywords.el if available; * isa/README, isar/README, isar/todo: updated; * generic/proof-script.el: pg-add-proof-element: removed accidential (?) dynamic scoping on proofbodyspan; handle proof-script-integral-proofs; * generic/proof-config.el: added proof-script-integral-proofs ("Whether the complete text after a goal confines the actual proof."); * isar/isar.el: proof-script-integral-proofs t; 2001-08-30 David Aspinall * ChangeLog: Updated. * CHANGES: Clarify 6.3.1 for multi file * isa/isabelle-system.el: Fix interrupt hook for PolyML 4 in recent Isabelle * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-shell.el: Add reassurance to interrupt warning to make Markus happier. * html/download.html: Note about XEmacs 21 and x-symbol * isa/isabelle-system.el: Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3). * CHANGES: More about invisible proofs and multiple files in Coq. X-symbol compat * generic/proof-x-symbol.el: Updates for recent version of X-symbol, which has no file called x-symbol-autoloads. * generic/proof-menu.el: Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings. * generic/proof.el: Add variable proof-previous-script-buffer * generic/proof-script.el: fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated * generic/proof-compat.el: Added implementation of remassq for FSF Emacs * generic/pg-user.el: pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment. 2001-08-30 David Aspinall * CHANGES: Clarify 6.3.1 for multi file * isa/isabelle-system.el: Fix interrupt hook for PolyML 4 in recent Isabelle * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-shell.el: Add reassurance to interrupt warning to make Markus happier. * html/download.html: Note about XEmacs 21 and x-symbol * isa/isabelle-system.el: Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3). * CHANGES: More about invisible proofs and multiple files in Coq. X-symbol compat * generic/proof-x-symbol.el: Updates for recent version of X-symbol, which has no file called x-symbol-autoloads. * generic/proof-menu.el: Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings. * generic/proof.el: Add variable proof-previous-script-buffer * generic/proof-script.el: fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated * generic/proof-compat.el: Added implementation of remassq for FSF Emacs * generic/pg-user.el: pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment. 2001-08-28 David Aspinall * doc/PG-adapting.texi, doc/ProofGeneral.texi: Fix web page for kit 2001-08-28 Pierre Courtieu * doc/ProofGeneral.texi: added something in the doc about coq-version-is-V7. * coq/coq.el: Added something in the doc about coq-version-is-V7, and made the setting of this variable more trustable with (concat coq-prog-name "-v"). 2001-08-28 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-script.el: Change of proof span type back to goalsave fix * lego/lego.el, coq/coq.el, phox/phox-fun.el, isar/isar.el: Change of proof span type back to goalsave * generic/proof-splash.el: Remove dependent setting of timeout, since bin calls different fn now. * bin/proofgeneral: Call function which always waits to prevent odd mode selection bug. * generic/proof-splash.el: Trivial * generic/proof-splash.el: Remove mention of toolbar variable. Make timeouts vary according to how started. * generic/proof-splash.el: Timeout happens as intended now, while loading some parts of PG. * html/header.html, html/proofgen.css: Improve stylesheet syntax, make menubar smaller 2001-08-17 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-script.el: Trim visibility implementation: - remove visibility specs and script portion records during undo - clear visibility specs on restart * generic/span-extent.el, generic/span-overlay.el: Add span-delete-action hook * CHANGES: Minibuffer contents bug fix * generic/proof-utils.el: Fix bug in proof-display-and-keep-buffer which had resulted in switching minibuffer windows buffer. 2001-08-16 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * doc/ProofGeneral.texi: Document visibility control * html/devel.html: Add link to browse files * html/download.html: Add link to browse package * html/develdownload.php: Add link to individual files * CHANGES: Move visibility item up, removed "in progress" * generic/proof-shell.el: Switch back to using goalsave spans in PBP code * generic/proof-config.el, generic/proof-toolbar.el: Add hide/show commands instead of make proofs visible * generic/proof-script.el: Generate intermediate proof span for contents of proof; other becomes 'goalsave again. Add idiom property. * generic/pg-user.el: Function name fixes, use idiom property in span for popup menu name. 2001-08-15 David Aspinall * html/gallery.php: Fix screenshots link * html/gallery: Fix again. * html/gallery: Fix link 2001-08-10 David Aspinall * ChangeLog: Updated. * CHANGES: Explain symptom properly * generic/proof-script.el: Use proof-looking-at-syntactic-context function from proof-syntax, as suggested by Markus * generic/proof-syntax.el: Found another instance of buffer-syntactic-context * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Put all in dist except pgkit * README: Rearrange list of assistants, note REGISTER. * FAQ: Remove note about 3.1 * BUGS: Comment about win32 XEmacs * generic/proof-compat.el: Workaround for buffer-syntactic-context bug in XEmacs 21.1 * generic/proof-script.el, isar/isar.el: Change buffer-syntactic-context -> proof-buffer-syntactic-context * etc/isar/XEmacsSyntacticContextProb.thy: Bug test case, note workaround date * etc/isar/XEmacsSyntacticContextProb.thy: Bug test case * CHANGES: Note of bug fix for buffer-syntactic-context 2001-08-09 Markus Wenzel * isa/x-symbol-isabelle.el: fixed potential regexp typo (!?); 2001-08-03 David Aspinall * CHANGES: Note about improved win32 support * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/fileshow.php: Fix link back to fileshow.php * html/fileshow.html: Renamed file * html/main.html: Fix screenshot link 2001-08-01 David Aspinall * doc/ProofGeneral.texi, doc/PG-adapting.texi: Update last updated, copyright * README.windows: Formatting * README: Update for 3.3 * ChangeLog: Updated. * html/screenshot.html, html/about.html, html/oldnews.html: Fix links to gallery * html/gallery.html: Deleted files. * html/gallery: Renamed file * html/gallery.html: Moved to .php * html/about.html: Fix typo * html/gallery.php, html/gallery.html: Renamed file * html/news.html: Added news * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * generic/proof-autoloads.el: Regenerate to remove Christophes patch * generic/proof-compat.el, generic/proof-site.el: Moved compat hack to proof-site * generic/proof-toolbar.el: Revert to removing and re-adding specifiers for toolbar, so that enablers work at least as well as they did before... * generic/proof-compat.el: Add a dummy version of package-provide for FSFEmacs. 2001-07-25 Christophe Raffalli * generic/proof-autoloads.el, generic/proof-splash.el, README.windows: *** empty log message *** * phox/phox.el, phox/phox-sym-lock.el, phox/phox-fun.el, generic/proof-splash.el, generic/proof-toolbar.el: Various changes for win32 compatibility 2001-07-23 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-menu.el: Prevent error msg in proof-display-some-buffers if response dead. * generic/proof-shell.el: Bug report from Robert Schneck. Make proof-shell-restart start shell. Goals display convention, not hack. 2001-07-09 David Aspinall * ChangeLog: Updated. * todo: TODO for proof-ass fixing added. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-toolbar.el: Clean for compile * generic/proof-menu.el: Clean for compile: new autload * generic/proof-autoloads.el: Refresh * generic/pg-xml.el, generic/pg-user.el: Clean-up compile * generic/proof-compat.el: Add require for arch flags, cleaner compilation. * generic/pg-pgip.el: Fix some bugs shown by byte comp * generic/proof-autoloads.el: Updated autoloads * generic/_pkg.el: Package file (old attempt -- not working) 2001-06-22 Christophe Raffalli * phox/phox.el: *** empty log message *** 2001-05-29 David Aspinall * html/main.html: Fix Coq link. * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * isa/Example.ML: Remove extra proof." * generic/proof-splash.el: Display screen only if called interactively * doc/ProofGeneral.texi: AF2 -> PhoX name change * etc/ProofGeneral.spec: Add REGISTER to doc files. * COPYING: Date 2001 * html/features.html: Fix layout and typo. * html/mailinglist.html: Include PHP file * REGISTER: Note about mailing list and registration. * html/mailinglist, html/mailinglist.php: Renamed file * html/mailinglist.html, html/mailinglist.php: PHP version. Also dont mention junk filters. 2001-05-18 Markus Wenzel * isar/isar-keywords.el: preliminary addition of "corollary"; 2001-05-16 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * doc/ProofGeneral.texi: Minor * bin/proofgeneral: Run the display splash command * generic/proof-config.el: Moved splash settings and basic custom groups elsewhere * CHANGES: splash changes. * generic/proof-site.el: Move loading of compatibility flag, autoloads, basic customization groups here. * generic/proof.el: Move autoloads loads to proof-site, invoke (proof-splash-message) * generic/proof-compat.el: Move emacs version compatibility flags to proof-site.el * generic/proof-splash.el: Move configuration from proof-config here. Make proof-splash-message display logo or print message. * etc/README: Doc of spec and menu, patch now removed 2001-05-08 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.menu: Fix case to match Mandrake menu. * ChangeLog: Updated. * etc/ProofGeneral.menu: Fix quotes. * html/functions.php3: Repair link via htmlshow.php * doc/PG-adapting.texi: Change info dir entry to appear next to Proof General entry. * ChangeLog: Updated. * html/develdownload.php: Set version tag for new release. * Makefile.devel: Change DEVELDOWNLOAD to edit correct file * ChangeLog: Updated. * etc/ProofGeneral.spec: Add a line to clear out build root. * ChangeLog: Updated. * Makefile.devel: Forgot to make BUILD dir. * ChangeLog: Updated. * Makefile.devel: Fix cut and past tab error * Makefile.devel: rpm target: Clean out rpmtopdir, and make subdirs again. Get full path to tar file * ChangeLog: Updated. * Makefile.devel: Clean out NAME, force link. * ChangeLog: Updated. * Makefile.devel: Include a few files from etc in the distribution, esp .spec file * etc/ProofGeneral.menu: *** empty log message *** * etc/ProofGeneral.patch: Deleted files. * ChangeLog: Updated. * doc/ProofGeneral.texi: Fix section title for makeinfo * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Dont make SRPM any more. Use rpm -tb to build binary package from tarball * CHANGES: Updates * etc/ProofGeneral.spec: Updates, removal of patch so that rpm -ta works * doc/ProofGeneral.texi: Updates for 3.3 * generic/proof-utils.el: Fixes for fontification in Xemacs 21.4 * generic/proof-site.el, generic/proof-syntax.el, generic/proof-shell.el, generic/proof-easy-config.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-config.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, generic/proof-compat.el: Copyright date updated * generic/README: Add Markus to list of authors * html/main.html: preliminary -> experimental * html/develdownload.php: No longer distrib SRPM * html/news.html: New news item 2001-05-03 David Aspinall * generic/proof-splash.el: change for Emacs compatibility and FSF/Xemacs update. Copyright update. * generic/proof-script.el: Emacs fix (extent->span). Copyright update. 2001-05-01 David Aspinall * ChangeLog: Updated. * doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi: Try to disable image for now * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/devel.html: Change link to kit * html/download.html: Change link to register page * html/feedback.html, html/index.shtml: Include php file * html/register, html/kit: Register and kit shortcuts * html/develdownload.html: Include php file * html/functions.php3: Link to php files instead of html * html/links, html/main, html/news, html/about, html/devel, html/doc, html/download, html/features: Include php instead of html * html/smallpage.php, html/htmlshow.php, html/index.php, html/develdownload.php, html/feedback.php, html/fileshow.php: Rename some html files php * html/index.html: Deleted files. 2001-04-10 Pierre Courtieu * coq/coq.el: Modification of proof-script-command-end-regexp to allow commands ended by ".eof" 2001-03-20 David Aspinall * ChangeLog: Updated. * html/main.html: Fixes to main page * html/footer.html: Change to my canonical www.dcs web address * html/main.html: Remove proofgeneral.org on main page * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.html: Set version tag for new release. * BUGS: strange buffer selection bug reported by Markus * doc/PG-adapting.texi: Updated magic 2001-03-20 Pierre Courtieu * coq/coq.el: Added the config var proof-script-command-end-regexp fot coq V7. 2001-03-20 David Aspinall * doc/Makefile.doc: Use PS fonts in PS file * generic/proof-shell.el: Remove temporary comments * generic/proof-config.el: Fix docstring * html/feedback.html, html/footer.html, html/functions.php3: Changes to use proofgen@dcs for now instead of broken proofgeneral.org * html/main.html: Fix to Coq web page 2001-03-19 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-26 Pierre Courtieu * coq/coq.el: minor change in coq.el to allow to force version of coq, with variable coq-version-is-V7 2001-02-20 Christophe Raffalli * phox/phox.el, phox/example.phx, phox/phox-extraction.el, phox/phox-fun.el, phox/phox-tags.el, html/develdownload.html, html/devel.html, phox/README, generic/proof-site.el, etc/ProofGeneral.spec: *** empty log message *** 2001-02-08 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-07 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: Set version tag for new release. 2001-02-07 Christophe Raffalli * phox/phox.el, phox/phox-font.el, phox/phox-fun.el, phox/phox-tags.el, phox/phox-extraction.el: *** empty log message *** 2001-02-06 David Aspinall * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-02-02 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-01 Markus Wenzel * doc/ProofGeneral.texi: updated thms_containing; 2001-02-01 Christophe Raffalli * phox/phox-sym-lock.el, phox/phox.el, phox/phox-font.el: *** empty log message *** 2001-01-24 Markus Wenzel * isa/x-symbol-isabelle.el: renamed \ to \ and \ to \; 2001-01-18 Markus Wenzel * isar/isar.el: proof-xsym-deactivate-command: use Library.gen_rems (op =) to avoid \\\\; 2001-01-18 Christophe Raffalli * phox/phox-extraction.el, phox/phox.el, phox/phox-fun.el, phox/phox-tags.el: *** empty log message *** 2001-01-12 Markus Wenzel * isa/isa.el: proof-string-match; 2001-01-12 David Aspinall * ChangeLog: Updated. * isa/isa.el: Fix loading thy mode fist problem: require proof-script since context menus are now added for response/goals buffer, which requires proof mode. 2001-01-12 Markus Wenzel * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: proof-string-match; 2001-01-12 Markus Wenzel * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: proof-string-match; 2001-01-11 Christophe Raffalli * phox/phox.el: *** empty log message *** 2001-01-11 Markus Wenzel * generic/proof-shell.el, generic/pg-xml.el, generic/proof-script.el: fixed format strings in message, error, etc. 2001-01-10 Markus Wenzel * isar/isar-syntax.el: proper font-lock of isar-keywords-proof-heading; * isa/x-symbol-isabelle.el: added \; 2001-01-09 Markus Wenzel * isa/x-symbol-isabelle.el: added \, \, \, \; 2001-01-05 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: Set version tag for new release. 2001-01-03 Markus Wenzel * isar/isar-keywords.el: added "recdef_tc";