2000-09-29 David Aspinall * 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 * coq/todo: added some comments in coq/todo 2000-09-29 David Aspinall * coq/coqtags, lego/legotags: Make default path to perl be /usr/bin/perl 2000-09-29 Pierre Courtieu * 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 * 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 * coq/todo: added some comments in coq/todo 2000-09-29 David Aspinall * coq/coqtags, lego/legotags: Make default path to perl be /usr/bin/perl 2000-09-29 Pierre Courtieu * 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 * 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 * coq/todo: added some comments in coq/todo 2000-09-29 David Aspinall * coq/coqtags, lego/legotags: Make default path to perl be /usr/bin/perl 2000-09-29 Pierre Courtieu * 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 * .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 * coq/todo: added some comments in coq/todo 2000-09-29 David Aspinall * coq/coqtags, lego/legotags: Make default path to perl be /usr/bin/perl 2000-09-29 Pierre Courtieu * 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 * 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 * coq/todo: added some comments in coq/todo 2000-09-29 David Aspinall * coq/coqtags, lego/legotags: Make default path to perl be /usr/bin/perl 2000-09-29 Pierre Courtieu * 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 * 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 * isar/isar.el: isar-web-page; 2000-09-28 David Aspinall * 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 * 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 * isar/isar.el: isar-web-page; 2000-09-28 David Aspinall * 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 * 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 * 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 * 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 * 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 * 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 * 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.... 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 * 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 * 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 * 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 * 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 * 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 * 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 * isar/interface, isa/interface: added -X option; 2000-09-20 David Aspinall * 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 * 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 * 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 * isa/interface-setup.el: more robust checking of xsymbol-home; 2000-09-18 Christophe Raffalli * 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 * 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 * isar/isar-keywords.el: complete set of keywords from IOA image; 2000-09-18 David Aspinall * 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 * 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 * isa/interface, isar/interface: isatool installfonts (for remote X-Symbol fonts); 2000-09-15 Christophe Raffalli * 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 * isa/x-symbol-isabelle.el: renamed \ to \; fixed glyph of \; * isa/x-symbol-isabelle.el: x-symbol-isabelle-electric-ignore: "~="; 2000-09-14 David Aspinall * 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 * 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 * 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 -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 -toolbar-entries, and move it and proof-toolbar-entries-default to proof-config to allow easier configuration. 2000-09-12 David Aspinall * 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 * isa/isabelle-system.el: proof-shell-pre-interrupt-hook for PolyML 3 only; 2000-09-11 David Aspinall * 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 * 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 * isar/isar-keywords.el: removed "of", "congs"; added "hints"; 2000-09-03 Markus Wenzel * isar/isar.el: removed unused variable C; 2000-09-02 Markus Wenzel * isar/interface, isa/interface: more quoting; 2000-08-30 Markus Wenzel * isar/isar.el: use isar-markup-ml; eliminated superficial semicolons; fixed proof-shell-quit-cmd; 2000-08-29 Markus Wenzel * isar/isar-syntax.el: syntax: "?" made word char; 2000-08-29 David Aspinall * 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 * 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 * 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 * 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 * isa/x-symbol-isabelle.el: more symbols; * isa/interface-setup.el: tuned x-symbol setup; 2000-08-16 Markus Wenzel * isar/isar-syntax.el: isar-keywords-proof-improper; * isar/isar-keywords.el: added isar-keywords-proof-improper; tuned; 2000-08-14 David Aspinall * 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 * 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 * isa/interface-setup.el: smart setup of X-Symbol mode; 2000-08-09 David Aspinall * 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 * 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 * 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 * 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 * isar/isar-syntax.el: fixed isar-goals-font-lock-keywords; * isar/isar-keywords.el: added "thm_deps", "overloaded"; 2000-07-26 Markus Wenzel * doc/ProofGeneral.texi: updated; * doc/docstring-magic.el: use proof-assistant-table instead of proof-assistants; 2000-07-26 David Aspinall * 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 * etc/test-schedule.txt: Note about need to test.. 2000-07-20 Markus Wenzel * generic/proof-site.el: proper evaluation of PROOFGENERAL_ASSISTANTS vs. proof-assistants; * generic/proof-easy-config.el: fixed comment; 2000-07-20 David Aspinall * isa/isa.el: Remove accidental testing setq left in. 2000-07-19 David Aspinall * 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 * isar/isar.el: use ML_command to avoid unwanted output; 2000-07-19 David Aspinall * isa/isa.el: reverting to last version 2000-07-19 fionam * isa/depends.ML, isa/isa.el: file for theorem dependencies 2000-07-17 Markus Wenzel * CHANGES: tuned; 2000-07-16 David Aspinall * 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 * 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 * 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 * 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 * isar/isar.el: tuned help-menu-entries; 2000-07-05 David Aspinall * 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 * 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 * 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 * isa/isabelle-system.el: quick-and-dirty t by default; 2000-07-03 David Aspinall * isa/isabelle-system.el: Patch to cope gracefully with empty list of Isabelle documents. 2000-07-01 Markus Wenzel * 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 * isar/isar-keywords.el: added method_setup; 2000-06-29 David Aspinall * 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 * 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 * generic/proof-script.el: Fix mark buffer atomic problem (caused multiple file oddity with Isar), for new parsing functions. 2000-06-22 David Aspinall * 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 * coq/coq.el, coq/coq-syntax.el: somme little changes to make undo work better 2000-06-19 David Aspinall * 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 * 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 * 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 * 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 * isar/todo: new indentation setup; 2000-06-09 David Aspinall * 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 * isa/isabelle-system.el: fixed show_sorts; * isar/isar.el: proof-shell-error-regexp; 2000-06-08 Markus Wenzel * 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 * 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 * 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 * 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 * 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 * isa/isa-syntax.el: fixed output syntax table; 2000-06-04 Markus Wenzel * 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 * 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 * coq/coq.el: Added 3 entries in the Coq menu: Print Check and Hints 2000-06-01 David Aspinall * 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 * 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 * isar/isar-syntax.el: improved isar-goals-font-lock-keywords; 2000-05-30 David Aspinall * 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 * isa/interface-setup.el: handle 'isa-x-symbol-enable vs. 'isar-x-symbol-enable; 2000-05-30 David Aspinall * 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 * isa/isabelle-system.el: defpacustom global-timing; 2000-05-30 David Aspinall * 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 * 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 * 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 * plastic/plastic.el, plastic/test.lf: fixed error in test.lf fixed conflict in plastic.el 2000-05-26 David Aspinall * 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 * isar/isar-syntax.el: isar-any-command-regexp; * isar/isar-keywords.el: isar-keywords-major; 2000-05-25 David Aspinall * 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- 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 * isar/isar-keywords.el: added "done"; 2000-05-22 Markus Wenzel * 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 * isar/isar-syntax.el, isar/isar.el: isar-verbatim-regexp: include \n; 2000-05-18 David Aspinall * todo: Updated. Noted that "first line" bug is more prevalent than thought. 2000-05-18 Markus Wenzel * isa/isa.el: Goals.enable/disable_pr: improved version for Isabelle99-1 (commented out); 2000-05-17 David Aspinall * 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 * 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 * ChangeLog.gz: Updated. 2000-05-16 Pierre Courtieu * 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 * 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 * 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 * 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 * 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 * generic/proof-config.el: Comments 2000-05-05 David Aspinall * 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 * 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 * 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 * 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 * 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 * 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 * 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 * 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 * 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 * isar/isar.el: fixed proof-mode-for-goals; 2000-04-07 David Aspinall * 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 * isar/x-symbol-isar.el, isa/x-symbol-isa.el: tuned \; added \, \, \; 2000-04-05 Markus Wenzel * 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 * isar/isar-keywords.el: added 'print_claset', 'print_simpset'; 2000-04-04 David Aspinall * 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.