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