2001-09-09 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Update for 3.4pre * html/footer.html: Remove validation stamp from footer, since its a lie. * CHANGES: No changes yet * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-09 David Aspinall * etc/ProofGeneral.spec, generic/proof-site.el: Set version tag for new release. * html/download.html: Trim page a bit * html/news.html, html/oldnews.html: Announce 3.3 * html/doc.html: Release 3-3. * etc/release-log.txt: Release date of 3-3. * html/download.html: Mention paper letter registrations. * html/download.html: Remove to be released line * doc/PG-adapting.texi: Update docs. 2001-09-06 Markus Wenzel * isa/interface, isar/interface: tuned usage; 2001-09-05 David Aspinall * doc/ProofGeneral.texi: Mention pg-toggle-visibility and its keybinding * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * generic/pg-metadata.el: Incomplete * doc/ProofGeneral.texi: Todo * CHANGES, todo: Updated * generic/proof-menu.el: Add keybindings for new commands for moving/navigating spans. * generic/proof-script.el: Fix problem with C-x C-v by copying buffer-file-name. Add children property to control spans. * generic/pg-user.el: Improved span moving and navigation commands. 2001-09-05 David Aspinall * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * generic/pg-metadata.el: Incomplete * doc/ProofGeneral.texi: Todo * CHANGES, todo: Updated * generic/proof-menu.el: Add keybindings for new commands for moving/navigating spans. * generic/proof-script.el: Fix problem with C-x C-v by copying buffer-file-name. Add children property to control spans. * generic/pg-user.el: Improved span moving and navigation commands. 2001-09-04 Markus Wenzel * isar/Example.thy: tuned proof text; added script version; * isa/interface, isar/interface: added option -P: actually start Proof General (default true); 2001-09-04 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/pg-xml.el: Issue parsing messages * generic/pg-user.el: Add commands to move spans up/down. Enable features only if experimental flag set * generic/proof-script.el: Nested proof spans are duplicable * generic/proof-config.el: Add experimental features setting * Makefile: Delete rogue elcs * CHANGES, INSTALL: Updates 2001-09-04 Markus Wenzel * isar/README: tuned; * isa/README, isar/README: no need to adjust the path to bash on the first line (due to /usr/bin/env); 2001-09-04 David Aspinall * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/pg-xml.el: Issue parsing messages * generic/pg-user.el: Add commands to move spans up/down. Enable features only if experimental flag set * generic/proof-script.el: Nested proof spans are duplicable * generic/proof-config.el: Add experimental features setting * Makefile: Delete rogue elcs * CHANGES, INSTALL: Updates 2001-09-04 Markus Wenzel * isar/README: tuned; * isa/README, isar/README: no need to adjust the path to bash on the first line (due to /usr/bin/env); 2001-09-03 David Aspinall * ChangeLog: Updated. * README.devel: Text * ChangeLog: Trim dups * README.windows: Add author * TODO, CHANGES: Updated * isa/Example.ML: Accidental commit; revert to original. * isar/isar.el: Set proof-goal-with-hole-regexp * generic/proof-config.el: Change colour of locked region. * generic/proof-shell.el: Fix bracket bug. * generic/proof-script.el: Show/hide all proofs: add redisplay for FSF Use new functions pg-set-span-helphighlights and pg-span-name to set help echo, balloon help, mouse highlight, and context menu. * generic/proof-depends.el: Use pg-set-span-helphightlights for unhighlighting. * generic/pg-user.el: Generalise context menu for other spans; grey out show/hide when unavailable. * html/main.html: Join paras * ChangeLog: Updated. * html/features.html: Text * html/features.html: Fix link to screenshot * html/doc.html: Improve layout * doc/PG-adapting.texi, doc/ProofGeneral.texi: Update version numbers, time stamps. * html/download.html: Typo. Update Emacs version to 20.7. * ChangeLog: Updated. * html/oldrel.php: Update branch * html/download.html: PHP file * html/oldrel.html, html/oldrel.php: Renamed file * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/download.html: Please try devel version * bin/proofgeneral, demoisa/demoisa.el: Accidental update; revert to previous * demoisa/README: Rearrange * twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/twelf-old.el, plastic/todo, twelf/example.elf, twelf/README, twelf/twelf-font.el, plastic/plastic.el, plastic/plastic-syntax.el, plastic/test.lf, phox/phox.el, plastic/README, phox/phox-outline.el, phox/phox-sym-lock.el, phox/phox-tags.el, phox/example.phx, phox/phox-extraction.el, phox/phox-font.el, phox/phox-fun.el, lego/readonly/readonly.l, papers/README, phox/README, lego/legotags, lego/todo, lego/x-symbol-lego.el, lego/example2.l, lego/lego.el, lego/lego-syntax.el, lego/BUGS, lego/example.l, lego/README, isar/todo, isar/isar.el, isar/isar-keywords.el, isar/isar-syntax.el, isar/BUGS, isar/Example.thy, isar/interface, isar/README, isa/todo, isa/x-symbol-isabelle.el, isa/isabelle-system.el, isa/thy-mode.el, isa/isa.el, isa/interface, isa/interface-setup.el, isa/isa-syntax.el, isa/depends.ML, isa/Example2.ML, isa/README, isa/BUGS, isa/Example.ML, isa/Example.thy, isa/Example-Xsym.ML, images/gimp/.cvsignore, images/gimp/scripts/proofgeneral.scm, images/use.8bit.xpm, images/use.xcf, images/use.xpm, images/undo.8bit.xpm, images/undo.xcf, images/undo.xpm, images/retract.xpm, images/state.8bit.xpm, images/state.xcf, images/state.xpm, images/restart.xpm, images/retract.8bit.xpm, images/retract.xcf, images/qed.xpm, images/restart.8bit.xpm, images/restart.xcf, images/pgicon.png, images/pgmini.xpm, images/qed.8bit.xpm, images/qed.xcf, images/pg-text.xcf, images/pg-text.8bit.gif, images/pg-text.gif, images/pg-text.jpg, images/next.xcf, images/next.xpm, images/notes.txt, images/next.8bit.xpm, images/lego-badge.xcf, images/isabelle_transparent.8bit.gif, images/isabelle_transparent.gif, images/isabelle_transparent.xcf, images/isabelle-badge.xcf, images/info.xpm, images/interrupt.8bit.xpm, images/interrupt.xcf, images/interrupt.xpm, images/help.xpm, images/info.8bit.xpm, images/info.xcf, images/goto.xcf, images/goto.xpm, images/help.8bit.xpm, images/help.xcf, images/goto.8bit.xpm, images/goal_large.xcf, images/goal.8bit.xpm, images/goal.xcf, images/goal.xpm, images/find.xpm, images/fireworks.xcf, images/find.8bit.xpm, images/find.xcf, images/context.xpm, images/coq-badge.xcf, images/command.xcf, images/command.xpm, images/context.8bit.xpm, images/context.xcf, images/abort.xpm, images/blank.xcf, images/command.8bit.xpm, images/abort.8bit.xpm, images/abort.xcf, images/README, images/ProofGeneral.jpg, images/ProofGeneral.xcf, images/ProofGeneral.8bit.gif, images/ProofGeneral.gif, images/.cvsignore, images/Makefile, html/projects/test.html, html/projects/thybrowse.html, html/projects/webreplay.html, html/projects/xmlpgip.html, html/projects/pgip.html, html/projects/pgml.html, html/projects/reelcase.html, html/projects/scrgen.html, html/projects/hol.html, html/projects/isapbp.html, html/projects/mm.html, html/projects/outline.html, html/projects/coqfile.html, html/projects/coqpbp.html, html/projects/corba.html, html/projects/acs.html, html/papers/pgtalk.pdf, html/papers/pgoutline.ps.gz, html/papers/pgoutline.pdf, html/images/whole-man.jpg, html/images/whole-man-thumb.jpg, html/images/silverrule.gif, html/images/vh40.gif, html/images/whip.jpg, html/images/whip-thumb.jpg, html/images/pg-text.gif, html/images/portrait.jpg, html/images/portrait-thumb.jpg, html/images/pg-lego-console.png, html/images/pg-lego-screenshot.png, html/images/pg-lego-thumb.png, html/images/pg-isar-thumb.png, html/images/pg-lego-console-thumb.png, html/images/pg-isar-screenshot.png, html/images/pg-isa-screenshot.png, html/images/pg-isa-thumb.png, html/images/pg-coq-thumb.png, html/images/isabelle.gif, html/images/lego-badge.gif, html/images/pg-coq-screenshot.png, html/images/canvaswallpaper.jpg, html/images/coq-badge.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf, html/images/isabelle-badge.gif, html/images/bullethole.gif, html/images/PG-small.jpg, html/images/ProofGeneral.jpg, html/images/.cvsignore, html/images/IsaPGscreen.jpg, .cvsignore, html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd, html/smallpage.php, html/screenshot.html, html/smallheader.html, html/smallpage.html, html/proofgen.css, html/register, html/register.html, html/screenshot, html/oldnews.html, html/oldrel.html, html/projects.html, html/news, html/news.html, html/notes.txt, html/main, html/main.html, html/mission.html, html/links, html/links.html, html/mailinglist, html/mailinglist.html, html/index.php, html/index.shtml, html/kit, html/kit.html, html/htmlshow.html, html/htmlshow.php, html/gallery.php, html/header.html, html/head.html, html/hits.html, html/fileshow.php, html/footer.html, html/functions.php3, html/gallery, html/features.html, html/feedback.html, html/feedback.php, html/download, html/download.html, html/elispmarkup.php3, html/features, html/develdownload.php, html/doc, html/doc.html, html/develdownload.html, html/cvsweb.conf, html/devel, html/devel.html, html/counter.php3, html/cvsweb.cgi, html/about, html/about.html, html/.cvsignore, html/ProofGeneralPortrait.eps.gz, hol98/example.sml, hol98/hol98.el, hol98/todo, hol98/x-symbol-hol98.el, generic/span.el, generic/texi-docstring-magic.el, hol98/README, generic/span-extent.el, generic/span-overlay.el, generic/proof.el, generic/proof-x-symbol.el, generic/proof-utils.el, generic/proof-syntax.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-splash.el, generic/proof-site.el, generic/proof-shell.el, generic/proof-script.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, etc/pgkit/xmltest1.xml, etc/pgkit/xmltest2.xml, generic/_pkg.el, generic/README, etc/patches/duplicated-short-messages-fix.txt, etc/patches/fix-attempt-for-eager-cleaning.txt, etc/lego/multiple/C.l, etc/lego/multiple/D.l, etc/lego/multiple/README, etc/lego/multiple/A.l, etc/lego/multiple/B.l, etc/lego/unsaved-goals.l, etc/lego/error-eg.l, etc/lego/lego-site.el, etc/lego/long-line-backslash.l, etc/isar/multiple/README, etc/lego/GoalGoal.l, etc/isar/multiple/A.thy, etc/isar/multiple/B.thy, etc/isar/multiple/C.thy, etc/isar/multiple/D.thy, etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README, etc/isar/XEmacsSyntacticContextProb.thy, etc/demoisa/README, etc/isar/Parsing.thy, etc/demoisa/A.ML, etc/demoisa/B.ML, etc/demoisa/C.ML, etc/demoisa/D.ML, etc/isa/multiple/foobar/foo.ML, etc/isa/thy/test.ML, etc/isa/multiple/D.thy, etc/isa/multiple/Err.ML, etc/isa/multiple/Err.thy, etc/isa/multiple/README, etc/isa/multiple/B.thy, etc/isa/multiple/C.ML, etc/isa/multiple/C.thy, etc/isa/multiple/D.ML, etc/isa/multiple/A.ML, etc/isa/multiple/A.thy, etc/isa/multiple/B.ML, etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/\backslashname/test.ML, etc/isa/\backslashname/test.thy, etc/isa/long-line-backslash.ML, etc/isa/message-test.ML, etc/isa/settings.ML, etc/isa/xsym.ML, etc/coq/multiple/c.v, etc/isa/goal-matching.ML, etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/.cvsignore, etc/coq/multiple/README, etc/coq/unnamed_thm.v, etc/testing-log.txt, etc/proofgeneral-domain.txt, etc/release-log.txt, etc/screenshot-notes.txt, etc/test-schedule.txt, etc/doc-notes.txt, etc/junk.el, etc/profiling.txt, etc/bug-notes.txt, etc/cvs-tips.txt, etc/debugging-tips.txt, etc/announce, etc/README, etc/TESTS, etc/ProofGeneral.menu, etc/ProofGeneral.spec, doc/dir, doc/docstring-magic.el, doc/localdir, doc/README.doc, doc/ProofGeneral.jpg, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile, demoisa/demoisa-easy.el, demoisa/demoisa.el, coq/todo, coq/x-symbol-coq.el, demoisa/README, coq/coqtags, coq/example.v, coq/coq.el, coq/BUGS, coq/coq-syntax.el, coq/README, acl2/example.acl2, acl2/x-symbol-acl2.el, bin/proofgeneral, acl2/acl2.el, acl2/README, todo, README.devel, README.windows, REGISTER, TODO, Makefile.xemacs, README, Makefile, Makefile.devel, FAQ, INSTALL, ChangeLog, COPYING, BUGS, CHANGES, AUTHORS: Updating branch * doc/ProofGeneral.texi: Note of what to do * generic/proof-script.el: Formatting * html/features.html: Mention hiding proofs. * etc/ProofGeneral.spec: Add specific READMEs. * etc/cvs-tips.txt: Note of secure alt to no password * etc/release-log.txt: Ready for release * etc/announce: Update for 3.3 * plastic/README, twelf/README, isa/README, isar/README, lego/README, phox/README, hol98/README, coq/README, generic/README, acl2/README: Add specific install instrs, rearrange. * INSTALL: Move specific install instructions into subdirs * isa/isa.el: Add settings for testing trace buffers. * CHANGES: Note about tracing buffers for developers * generic/proof-shell.el: Added handling of tracing buffers using proof-shell-spill-output-regexp. * generic/proof-config.el: Added proof-shell-spill-output-regexp 2001-09-03 David Aspinall * README.devel: Text * ChangeLog: Trim dups * README.windows: Add author * TODO, CHANGES: Updated * isa/Example.ML: Accidental commit; revert to original. * isar/isar.el: Set proof-goal-with-hole-regexp * generic/proof-config.el: Change colour of locked region. * generic/proof-shell.el: Fix bracket bug. * generic/proof-script.el: Show/hide all proofs: add redisplay for FSF Use new functions pg-set-span-helphighlights and pg-span-name to set help echo, balloon help, mouse highlight, and context menu. * generic/proof-depends.el: Use pg-set-span-helphightlights for unhighlighting. * generic/pg-user.el: Generalise context menu for other spans; grey out show/hide when unavailable. * html/main.html: Join paras * ChangeLog: Updated. * html/features.html: Text * html/features.html: Fix link to screenshot * html/doc.html: Improve layout * doc/PG-adapting.texi, doc/ProofGeneral.texi: Update version numbers, time stamps. * html/download.html: Typo. Update Emacs version to 20.7. * ChangeLog: Updated. * html/oldrel.php: Update branch * html/download.html: PHP file * html/oldrel.html, html/oldrel.php: Renamed file * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/download.html: Please try devel version * bin/proofgeneral, demoisa/demoisa.el: Accidental update; revert to previous * demoisa/README: Rearrange * twelf/twelf.el, twelf/x-symbol-twelf.el, twelf/twelf-old.el, plastic/todo, twelf/example.elf, twelf/README, twelf/twelf-font.el, plastic/plastic.el, plastic/plastic-syntax.el, plastic/test.lf, phox/phox.el, plastic/README, phox/phox-outline.el, phox/phox-sym-lock.el, phox/phox-tags.el, phox/example.phx, phox/phox-extraction.el, phox/phox-font.el, phox/phox-fun.el, lego/readonly/readonly.l, papers/README, phox/README, lego/legotags, lego/todo, lego/x-symbol-lego.el, lego/example2.l, lego/lego.el, lego/lego-syntax.el, lego/BUGS, lego/example.l, lego/README, isar/todo, isar/isar.el, isar/isar-keywords.el, isar/isar-syntax.el, isar/BUGS, isar/Example.thy, isar/interface, isar/README, isa/todo, isa/x-symbol-isabelle.el, isa/isabelle-system.el, isa/thy-mode.el, isa/isa.el, isa/interface, isa/interface-setup.el, isa/isa-syntax.el, isa/depends.ML, isa/Example2.ML, isa/README, isa/BUGS, isa/Example.ML, isa/Example.thy, isa/Example-Xsym.ML, images/gimp/.cvsignore, images/gimp/scripts/proofgeneral.scm, images/use.8bit.xpm, images/use.xcf, images/use.xpm, images/undo.8bit.xpm, images/undo.xcf, images/undo.xpm, images/retract.xpm, images/state.8bit.xpm, images/state.xcf, images/state.xpm, images/restart.xpm, images/retract.8bit.xpm, images/retract.xcf, images/qed.xpm, images/restart.8bit.xpm, images/restart.xcf, images/pgicon.png, images/pgmini.xpm, images/qed.8bit.xpm, images/qed.xcf, images/pg-text.xcf, images/pg-text.8bit.gif, images/pg-text.gif, images/pg-text.jpg, images/next.xcf, images/next.xpm, images/notes.txt, images/next.8bit.xpm, images/lego-badge.xcf, images/isabelle_transparent.8bit.gif, images/isabelle_transparent.gif, images/isabelle_transparent.xcf, images/isabelle-badge.xcf, images/info.xpm, images/interrupt.8bit.xpm, images/interrupt.xcf, images/interrupt.xpm, images/help.xpm, images/info.8bit.xpm, images/info.xcf, images/goto.xcf, images/goto.xpm, images/help.8bit.xpm, images/help.xcf, images/goto.8bit.xpm, images/goal_large.xcf, images/goal.8bit.xpm, images/goal.xcf, images/goal.xpm, images/find.xpm, images/fireworks.xcf, images/find.8bit.xpm, images/find.xcf, images/context.xpm, images/coq-badge.xcf, images/command.xcf, images/command.xpm, images/context.8bit.xpm, images/context.xcf, images/abort.xpm, images/blank.xcf, images/command.8bit.xpm, images/abort.8bit.xpm, images/abort.xcf, images/README, images/ProofGeneral.jpg, images/ProofGeneral.xcf, images/ProofGeneral.8bit.gif, images/ProofGeneral.gif, images/.cvsignore, images/Makefile, html/projects/test.html, html/projects/thybrowse.html, html/projects/webreplay.html, html/projects/xmlpgip.html, html/projects/pgip.html, html/projects/pgml.html, html/projects/reelcase.html, html/projects/scrgen.html, html/projects/hol.html, html/projects/isapbp.html, html/projects/mm.html, html/projects/outline.html, html/projects/coqfile.html, html/projects/coqpbp.html, html/projects/corba.html, html/projects/acs.html, html/papers/pgtalk.pdf, html/papers/pgoutline.ps.gz, html/papers/pgoutline.pdf, html/images/whole-man.jpg, html/images/whole-man-thumb.jpg, html/images/silverrule.gif, html/images/vh40.gif, html/images/whip.jpg, html/images/whip-thumb.jpg, html/images/pg-text.gif, html/images/portrait.jpg, html/images/portrait-thumb.jpg, html/images/pg-lego-console.png, html/images/pg-lego-screenshot.png, html/images/pg-lego-thumb.png, html/images/pg-isar-thumb.png, html/images/pg-lego-console-thumb.png, html/images/pg-isar-screenshot.png, html/images/pg-isa-screenshot.png, html/images/pg-isa-thumb.png, html/images/pg-coq-thumb.png, html/images/isabelle.gif, html/images/lego-badge.gif, html/images/pg-coq-screenshot.png, html/images/canvaswallpaper.jpg, html/images/coq-badge.gif, html/images/coqlogo4.gif, html/images/coqlogo4.xcf, html/images/isabelle-badge.gif, html/images/bullethole.gif, html/images/PG-small.jpg, html/images/ProofGeneral.jpg, html/images/.cvsignore, html/images/IsaPGscreen.jpg, .cvsignore, html/Kit/dtd/pgip.dtd, html/Kit/dtd/pgml.dtd, html/smallpage.php, html/screenshot.html, html/smallheader.html, html/smallpage.html, html/proofgen.css, html/register, html/register.html, html/screenshot, html/oldnews.html, html/oldrel.html, html/projects.html, html/news, html/news.html, html/notes.txt, html/main, html/main.html, html/mission.html, html/links, html/links.html, html/mailinglist, html/mailinglist.html, html/index.php, html/index.shtml, html/kit, html/kit.html, html/htmlshow.html, html/htmlshow.php, html/gallery.php, html/header.html, html/head.html, html/hits.html, html/fileshow.php, html/footer.html, html/functions.php3, html/gallery, html/features.html, html/feedback.html, html/feedback.php, html/download, html/download.html, html/elispmarkup.php3, html/features, html/develdownload.php, html/doc, html/doc.html, html/develdownload.html, html/cvsweb.conf, html/devel, html/devel.html, html/counter.php3, html/cvsweb.cgi, html/about, html/about.html, html/.cvsignore, html/ProofGeneralPortrait.eps.gz, hol98/example.sml, hol98/hol98.el, hol98/todo, hol98/x-symbol-hol98.el, generic/span.el, generic/texi-docstring-magic.el, hol98/README, generic/span-extent.el, generic/span-overlay.el, generic/proof.el, generic/proof-x-symbol.el, generic/proof-utils.el, generic/proof-syntax.el, generic/proof-system.el, generic/proof-toolbar.el, generic/proof-splash.el, generic/proof-site.el, generic/proof-shell.el, generic/proof-script.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-depends.el, generic/proof-easy-config.el, generic/proof-config.el, generic/proof-autoloads.el, generic/proof-compat.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, etc/pgkit/xmltest1.xml, etc/pgkit/xmltest2.xml, generic/_pkg.el, generic/README, etc/patches/duplicated-short-messages-fix.txt, etc/patches/fix-attempt-for-eager-cleaning.txt, etc/lego/multiple/C.l, etc/lego/multiple/D.l, etc/lego/multiple/README, etc/lego/multiple/A.l, etc/lego/multiple/B.l, etc/lego/unsaved-goals.l, etc/lego/error-eg.l, etc/lego/lego-site.el, etc/lego/long-line-backslash.l, etc/isar/multiple/README, etc/lego/GoalGoal.l, etc/isar/multiple/A.thy, etc/isar/multiple/B.thy, etc/isar/multiple/C.thy, etc/isar/multiple/D.thy, etc/isar/bad1.thy, etc/isar/bad2.thy, etc/isar/README, etc/isar/XEmacsSyntacticContextProb.thy, etc/demoisa/README, etc/isar/Parsing.thy, etc/demoisa/A.ML, etc/demoisa/B.ML, etc/demoisa/C.ML, etc/demoisa/D.ML, etc/isa/multiple/foobar/foo.ML, etc/isa/thy/test.ML, etc/isa/multiple/D.thy, etc/isa/multiple/Err.ML, etc/isa/multiple/Err.thy, etc/isa/multiple/README, etc/isa/multiple/B.thy, etc/isa/multiple/C.ML, etc/isa/multiple/C.thy, etc/isa/multiple/D.ML, etc/isa/multiple/A.ML, etc/isa/multiple/A.thy, etc/isa/multiple/B.ML, etc/isa/depends/Usedepends.ML, etc/isa/depends/Usedepends.thy, etc/isa/depends/Fib.ML, etc/isa/depends/Fib.thy, etc/isa/depends/Primes.ML, etc/isa/depends/Primes.thy, etc/isa/\backslashname/test.ML, etc/isa/\backslashname/test.thy, etc/isa/long-line-backslash.ML, etc/isa/message-test.ML, etc/isa/settings.ML, etc/isa/xsym.ML, etc/coq/multiple/c.v, etc/isa/goal-matching.ML, etc/coq/multiple/a.v, etc/coq/multiple/b.v, etc/coq/multiple/.cvsignore, etc/coq/multiple/README, etc/coq/unnamed_thm.v, etc/testing-log.txt, etc/proofgeneral-domain.txt, etc/release-log.txt, etc/screenshot-notes.txt, etc/test-schedule.txt, etc/doc-notes.txt, etc/junk.el, etc/profiling.txt, etc/bug-notes.txt, etc/cvs-tips.txt, etc/debugging-tips.txt, etc/announce, etc/README, etc/TESTS, etc/ProofGeneral.menu, etc/ProofGeneral.spec, doc/dir, doc/docstring-magic.el, doc/localdir, doc/README.doc, doc/ProofGeneral.jpg, doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi, doc/.cvsignore, doc/Makefile, demoisa/demoisa-easy.el, demoisa/demoisa.el, coq/todo, coq/x-symbol-coq.el, demoisa/README, coq/coqtags, coq/example.v, coq/coq.el, coq/BUGS, coq/coq-syntax.el, coq/README, acl2/example.acl2, acl2/x-symbol-acl2.el, bin/proofgeneral, acl2/acl2.el, acl2/README, todo, README.devel, README.windows, REGISTER, TODO, Makefile.xemacs, README, Makefile, Makefile.devel, FAQ, INSTALL, ChangeLog, COPYING, BUGS, CHANGES, AUTHORS: Updating branch * doc/ProofGeneral.texi: Note of what to do * generic/proof-script.el: Formatting * html/features.html: Mention hiding proofs. * etc/ProofGeneral.spec: Add specific READMEs. * etc/cvs-tips.txt: Note of secure alt to no password * etc/release-log.txt: Ready for release * etc/announce: Update for 3.3 * plastic/README, twelf/README, isa/README, isar/README, lego/README, phox/README, hol98/README, coq/README, generic/README, acl2/README: Add specific install instrs, rearrange. * INSTALL: Move specific install instructions into subdirs * isa/isa.el: Add settings for testing trace buffers. * CHANGES: Note about tracing buffers for developers * generic/proof-shell.el: Added handling of tracing buffers using proof-shell-spill-output-regexp. * generic/proof-config.el: Added proof-shell-spill-output-regexp 2001-09-02 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-09-02 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-08-31 Markus Wenzel * isa/interface, isar/interface: handle relative heap paths gracefully; * isar/isar-keywords.el: back to *official* Isabelle99-2 (later Isabelle dists will provide their own copy of this file); 2001-08-31 David Aspinall * CHANGES: Improved explanation * doc/ProofGeneral.texi: Something about dependencies feature * CHANGES: Added note about dependency feature. * generic/proof-depends.el: (Almost) complete rewrite * generic/proof-autoloads.el: Updated * generic/proof-script.el: Move theorem dependency code into proof-depends.el. Added 'controlspan property to proof body spans: action will be controlled from the control span. (The 'goalsave is the parent). Replace 'highlight face with 'proof-mouse-highlight-face throughout. * generic/pg-user.el: Added copy command, call to dependency menu if proof-depends is loaded. * isa/depends.ML: Add simulations of more qed commands, also sort and uniquify dependencies. * generic/proof-config.el: Add new proof-mouse-highlight-face to use instead of default. Fix dependency faces. 2001-08-31 Markus Wenzel * isar/isar-keywords.el: new commands (proof terms, code generator); 2001-08-31 David Aspinall * ChangeLog: Remove duplicate entries * generic/proof-config.el: Add faces for theorem dependencies. * etc/coq/multiple/README: Explanation * AUTHORS: Add DvO to list * AUTHORS: Add Christophe to list * coq/coq.el: Add auto-compile-vos experimental setting for automatic multiple files. * BUGS: Remove minibuffer bug * isa/thy-mode.el: Fix for names of functions in proof-depends * isa/isa.el: Add setting for turning on theorem dependency tracking * isa/depends.ML: Update for Isabelle99-2 * generic/proof-depends.el, generic/proof-script.el: Clean up of proof-depends * generic/proof-menu.el: Skip settings which have no PA command in proof-assistant-settings-cmd * generic/proof-shell.el: Add proof-shell-kill-function-hooks 2001-08-30 Markus Wenzel * isa/interface, isar/interface: include ISABELLE_HOME_USER/etc/isar-keywords.el or ISABELLE_HOME/etc/isar-keywords.el if available; * isa/README, isar/README, isar/todo: updated; * generic/proof-script.el: pg-add-proof-element: removed accidential (?) dynamic scoping on proofbodyspan; handle proof-script-integral-proofs; * generic/proof-config.el: added proof-script-integral-proofs ("Whether the complete text after a goal confines the actual proof."); * isar/isar.el: proof-script-integral-proofs t; 2001-08-30 David Aspinall * ChangeLog: Updated. * CHANGES: Clarify 6.3.1 for multi file * isa/isabelle-system.el: Fix interrupt hook for PolyML 4 in recent Isabelle * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-shell.el: Add reassurance to interrupt warning to make Markus happier. * html/download.html: Note about XEmacs 21 and x-symbol * isa/isabelle-system.el: Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3). * CHANGES: More about invisible proofs and multiple files in Coq. X-symbol compat * generic/proof-x-symbol.el: Updates for recent version of X-symbol, which has no file called x-symbol-autoloads. * generic/proof-menu.el: Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings. * generic/proof.el: Add variable proof-previous-script-buffer * generic/proof-script.el: fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated * generic/proof-compat.el: Added implementation of remassq for FSF Emacs * generic/pg-user.el: pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment. 2001-08-30 David Aspinall * CHANGES: Clarify 6.3.1 for multi file * isa/isabelle-system.el: Fix interrupt hook for PolyML 4 in recent Isabelle * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-shell.el: Add reassurance to interrupt warning to make Markus happier. * html/download.html: Note about XEmacs 21 and x-symbol * isa/isabelle-system.el: Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3). * CHANGES: More about invisible proofs and multiple files in Coq. X-symbol compat * generic/proof-x-symbol.el: Updates for recent version of X-symbol, which has no file called x-symbol-autoloads. * generic/proof-menu.el: Add :eval form for defpacustom to define PA-specific PG settings as well as PA settings. * generic/proof.el: Add variable proof-previous-script-buffer * generic/proof-script.el: fixes for FSF Emacs for searching for goal span (don't call goal-command-p on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated * generic/proof-compat.el: Added implementation of remassq for FSF Emacs * generic/pg-user.el: pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment. 2001-08-28 David Aspinall * doc/PG-adapting.texi, doc/ProofGeneral.texi: Fix web page for kit 2001-08-28 Pierre Courtieu * doc/ProofGeneral.texi: added something in the doc about coq-version-is-V7. * coq/coq.el: Added something in the doc about coq-version-is-V7, and made the setting of this variable more trustable with (concat coq-prog-name "-v"). 2001-08-28 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-script.el: Change of proof span type back to goalsave fix * lego/lego.el, coq/coq.el, phox/phox-fun.el, isar/isar.el: Change of proof span type back to goalsave * generic/proof-splash.el: Remove dependent setting of timeout, since bin calls different fn now. * bin/proofgeneral: Call function which always waits to prevent odd mode selection bug. * generic/proof-splash.el: Trivial * generic/proof-splash.el: Remove mention of toolbar variable. Make timeouts vary according to how started. * generic/proof-splash.el: Timeout happens as intended now, while loading some parts of PG. * html/header.html, html/proofgen.css: Improve stylesheet syntax, make menubar smaller 2001-08-17 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-script.el: Trim visibility implementation: - remove visibility specs and script portion records during undo - clear visibility specs on restart * generic/span-extent.el, generic/span-overlay.el: Add span-delete-action hook * CHANGES: Minibuffer contents bug fix * generic/proof-utils.el: Fix bug in proof-display-and-keep-buffer which had resulted in switching minibuffer windows buffer. 2001-08-16 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * doc/ProofGeneral.texi: Document visibility control * html/devel.html: Add link to browse files * html/download.html: Add link to browse package * html/develdownload.php: Add link to individual files * CHANGES: Move visibility item up, removed "in progress" * generic/proof-shell.el: Switch back to using goalsave spans in PBP code * generic/proof-config.el, generic/proof-toolbar.el: Add hide/show commands instead of make proofs visible * generic/proof-script.el: Generate intermediate proof span for contents of proof; other becomes 'goalsave again. Add idiom property. * generic/pg-user.el: Function name fixes, use idiom property in span for popup menu name. 2001-08-15 David Aspinall * html/gallery.php: Fix screenshots link * html/gallery: Fix again. * html/gallery: Fix link 2001-08-10 David Aspinall * ChangeLog: Updated. * CHANGES: Explain symptom properly * generic/proof-script.el: Use proof-looking-at-syntactic-context function from proof-syntax, as suggested by Markus * generic/proof-syntax.el: Found another instance of buffer-syntactic-context * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Put all in dist except pgkit * README: Rearrange list of assistants, note REGISTER. * FAQ: Remove note about 3.1 * BUGS: Comment about win32 XEmacs * generic/proof-compat.el: Workaround for buffer-syntactic-context bug in XEmacs 21.1 * generic/proof-script.el, isar/isar.el: Change buffer-syntactic-context -> proof-buffer-syntactic-context * etc/isar/XEmacsSyntacticContextProb.thy: Bug test case, note workaround date * etc/isar/XEmacsSyntacticContextProb.thy: Bug test case * CHANGES: Note of bug fix for buffer-syntactic-context 2001-08-09 Markus Wenzel * isa/x-symbol-isabelle.el: fixed potential regexp typo (!?); 2001-08-03 David Aspinall * CHANGES: Note about improved win32 support * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/fileshow.php: Fix link back to fileshow.php * html/fileshow.html: Renamed file * html/main.html: Fix screenshot link 2001-08-01 David Aspinall * doc/ProofGeneral.texi, doc/PG-adapting.texi: Update last updated, copyright * README.windows: Formatting * README: Update for 3.3 * ChangeLog: Updated. * html/screenshot.html, html/about.html, html/oldnews.html: Fix links to gallery * html/gallery.html: Deleted files. * html/gallery: Renamed file * html/gallery.html: Moved to .php * html/about.html: Fix typo * html/gallery.php, html/gallery.html: Renamed file * html/news.html: Added news * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * generic/proof-autoloads.el: Regenerate to remove Christophes patch * generic/proof-compat.el, generic/proof-site.el: Moved compat hack to proof-site * generic/proof-toolbar.el: Revert to removing and re-adding specifiers for toolbar, so that enablers work at least as well as they did before... * generic/proof-compat.el: Add a dummy version of package-provide for FSFEmacs. 2001-07-25 Christophe Raffalli * generic/proof-autoloads.el, generic/proof-splash.el, README.windows: *** empty log message *** * phox/phox.el, phox/phox-sym-lock.el, phox/phox-fun.el, generic/proof-splash.el, generic/proof-toolbar.el: Various changes for win32 compatibility 2001-07-23 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-menu.el: Prevent error msg in proof-display-some-buffers if response dead. * generic/proof-shell.el: Bug report from Robert Schneck. Make proof-shell-restart start shell. Goals display convention, not hack. 2001-07-09 David Aspinall * ChangeLog: Updated. * todo: TODO for proof-ass fixing added. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * generic/proof-toolbar.el: Clean for compile * generic/proof-menu.el: Clean for compile: new autload * generic/proof-autoloads.el: Refresh * generic/pg-xml.el, generic/pg-user.el: Clean-up compile * generic/proof-compat.el: Add require for arch flags, cleaner compilation. * generic/pg-pgip.el: Fix some bugs shown by byte comp * generic/proof-autoloads.el: Updated autoloads * generic/_pkg.el: Package file (old attempt -- not working) 2001-06-22 Christophe Raffalli * phox/phox.el: *** empty log message *** 2001-05-29 David Aspinall * html/main.html: Fix Coq link. * ChangeLog: Updated. * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: Set version tag for new release. * isa/Example.ML: Remove extra proof." * generic/proof-splash.el: Display screen only if called interactively * doc/ProofGeneral.texi: AF2 -> PhoX name change * etc/ProofGeneral.spec: Add REGISTER to doc files. * COPYING: Date 2001 * html/features.html: Fix layout and typo. * html/mailinglist.html: Include PHP file * REGISTER: Note about mailing list and registration. * html/mailinglist, html/mailinglist.php: Renamed file * html/mailinglist.html, html/mailinglist.php: PHP version. Also dont mention junk filters. 2001-05-18 Markus Wenzel * isar/isar-keywords.el: preliminary addition of "corollary"; 2001-05-16 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.php: Set version tag for new release. * doc/ProofGeneral.texi: Minor * bin/proofgeneral: Run the display splash command * generic/proof-config.el: Moved splash settings and basic custom groups elsewhere * CHANGES: splash changes. * generic/proof-site.el: Move loading of compatibility flag, autoloads, basic customization groups here. * generic/proof.el: Move autoloads loads to proof-site, invoke (proof-splash-message) * generic/proof-compat.el: Move emacs version compatibility flags to proof-site.el * generic/proof-splash.el: Move configuration from proof-config here. Make proof-splash-message display logo or print message. * etc/README: Doc of spec and menu, patch now removed 2001-05-08 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.menu: Fix case to match Mandrake menu. * ChangeLog: Updated. * etc/ProofGeneral.menu: Fix quotes. * html/functions.php3: Repair link via htmlshow.php * doc/PG-adapting.texi: Change info dir entry to appear next to Proof General entry. * ChangeLog: Updated. * html/develdownload.php: Set version tag for new release. * Makefile.devel: Change DEVELDOWNLOAD to edit correct file * ChangeLog: Updated. * etc/ProofGeneral.spec: Add a line to clear out build root. * ChangeLog: Updated. * Makefile.devel: Forgot to make BUILD dir. * ChangeLog: Updated. * Makefile.devel: Fix cut and past tab error * Makefile.devel: rpm target: Clean out rpmtopdir, and make subdirs again. Get full path to tar file * ChangeLog: Updated. * Makefile.devel: Clean out NAME, force link. * ChangeLog: Updated. * Makefile.devel: Include a few files from etc in the distribution, esp .spec file * etc/ProofGeneral.menu: *** empty log message *** * etc/ProofGeneral.patch: Deleted files. * ChangeLog: Updated. * doc/ProofGeneral.texi: Fix section title for makeinfo * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el: Set version tag for new release. * Makefile.devel: Dont make SRPM any more. Use rpm -tb to build binary package from tarball * CHANGES: Updates * etc/ProofGeneral.spec: Updates, removal of patch so that rpm -ta works * doc/ProofGeneral.texi: Updates for 3.3 * generic/proof-utils.el: Fixes for fontification in Xemacs 21.4 * generic/proof-site.el, generic/proof-syntax.el, generic/proof-shell.el, generic/proof-easy-config.el, generic/proof-indent.el, generic/proof-menu.el, generic/proof-config.el, generic/pg-pgip.el, generic/pg-user.el, generic/pg-xml.el, generic/proof-compat.el: Copyright date updated * generic/README: Add Markus to list of authors * html/main.html: preliminary -> experimental * html/develdownload.php: No longer distrib SRPM * html/news.html: New news item 2001-05-03 David Aspinall * generic/proof-splash.el: change for Emacs compatibility and FSF/Xemacs update. Copyright update. * generic/proof-script.el: Emacs fix (extent->span). Copyright update. 2001-05-01 David Aspinall * ChangeLog: Updated. * doc/ProofGeneral.texi, doc/Makefile.doc, doc/PG-adapting.texi: Try to disable image for now * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el: Set version tag for new release. * html/devel.html: Change link to kit * html/download.html: Change link to register page * html/feedback.html, html/index.shtml: Include php file * html/register, html/kit: Register and kit shortcuts * html/develdownload.html: Include php file * html/functions.php3: Link to php files instead of html * html/links, html/main, html/news, html/about, html/devel, html/doc, html/download, html/features: Include php instead of html * html/smallpage.php, html/htmlshow.php, html/index.php, html/develdownload.php, html/feedback.php, html/fileshow.php: Rename some html files php * html/index.html: Deleted files. 2001-04-10 Pierre Courtieu * coq/coq.el: Modification of proof-script-command-end-regexp to allow commands ended by ".eof" 2001-03-20 David Aspinall * ChangeLog: Updated. * html/main.html: Fixes to main page * html/footer.html: Change to my canonical www.dcs web address * html/main.html: Remove proofgeneral.org on main page * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, generic/proof-site.el, html/develdownload.html: Set version tag for new release. * BUGS: strange buffer selection bug reported by Markus * doc/PG-adapting.texi: Updated magic 2001-03-20 Pierre Courtieu * coq/coq.el: Added the config var proof-script-command-end-regexp fot coq V7. 2001-03-20 David Aspinall * doc/Makefile.doc: Use PS fonts in PS file * generic/proof-shell.el: Remove temporary comments * generic/proof-config.el: Fix docstring * html/feedback.html, html/footer.html, html/functions.php3: Changes to use proofgen@dcs for now instead of broken proofgeneral.org * html/main.html: Fix to Coq web page 2001-03-19 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-26 Pierre Courtieu * coq/coq.el: minor change in coq.el to allow to force version of coq, with variable coq-version-is-V7 2001-02-20 Christophe Raffalli * phox/phox.el, phox/example.phx, phox/phox-extraction.el, phox/phox-fun.el, phox/phox-tags.el, html/develdownload.html, html/devel.html, phox/README, generic/proof-site.el, etc/ProofGeneral.spec: *** empty log message *** 2001-02-08 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-07 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, html/devel.html, html/develdownload.html, generic/proof-site.el: Set version tag for new release. 2001-02-07 Christophe Raffalli * phox/phox.el, phox/phox-font.el, phox/phox-fun.el, phox/phox-tags.el, phox/phox-extraction.el: *** empty log message *** 2001-02-06 David Aspinall * etc/ProofGeneral.spec, html/develdownload.html, html/devel.html, generic/proof-site.el: Set version tag for new release. 2001-02-02 Christophe Raffalli * phox/phox-font.el: *** empty log message *** 2001-02-01 Markus Wenzel * doc/ProofGeneral.texi: updated thms_containing; 2001-02-01 Christophe Raffalli * phox/phox-sym-lock.el, phox/phox.el, phox/phox-font.el: *** empty log message *** 2001-01-24 Markus Wenzel * isa/x-symbol-isabelle.el: renamed \ to \ and \ to \; 2001-01-18 Markus Wenzel * isar/isar.el: proof-xsym-deactivate-command: use Library.gen_rems (op =) to avoid \\\\; 2001-01-18 Christophe Raffalli * phox/phox-extraction.el, phox/phox.el, phox/phox-fun.el, phox/phox-tags.el: *** empty log message *** 2001-01-12 Markus Wenzel * isa/isa.el: proof-string-match; 2001-01-12 David Aspinall * ChangeLog: Updated. * isa/isa.el: Fix loading thy mode fist problem: require proof-script since context menus are now added for response/goals buffer, which requires proof mode. 2001-01-12 Markus Wenzel * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: proof-string-match; 2001-01-12 Markus Wenzel * isa/isabelle-system.el, isar/isar.el, isar/isar-syntax.el: proof-string-match; 2001-01-11 Christophe Raffalli * phox/phox.el: *** empty log message *** 2001-01-11 Markus Wenzel * generic/proof-shell.el, generic/pg-xml.el, generic/proof-script.el: fixed format strings in message, error, etc. 2001-01-10 Markus Wenzel * isar/isar-syntax.el: proper font-lock of isar-keywords-proof-heading; * isa/x-symbol-isabelle.el: added \; 2001-01-09 Markus Wenzel * isa/x-symbol-isabelle.el: added \, \, \, \; 2001-01-05 David Aspinall * ChangeLog: Updated. * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.html, html/devel.html: Set version tag for new release. 2001-01-03 Markus Wenzel * isar/isar-keywords.el: added "recdef_tc";