diff options
Diffstat (limited to 'todo')
| -rw-r--r-- | todo | 761 |
1 files changed, 761 insertions, 0 deletions
@@ -0,0 +1,761 @@ +-*- mode:outline -*- + +* Proof General Low-level List of Things to Do + +$Id$ + +This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. + +** 0. Contents + + 1. Priorities + 2. Things to do in the generic interface + 3. Things to do for the documentation + 4. Emacs issues + 5. Things to do for Proof-by-Pointing + 6. Things to do for Web Pages, Distribution + 7. Future improvements to take advantage of newer Emacsen + 8. Bugs in other software beyond our control + 9. Stable version release checklist +10. Things to do for Proof General Project + + See <prover>/todo for things to do for each prover. + +** 1. Priorities + +A (High) e.g. to be fixed ASAP for next pre-release +B e.g. to be fixed before next release +C (Medium) e.g. would be nice to fix before next release; not crucial +D e.g. desirable to fix at some point +X (Low) e.g. probably not worth spending time on + + +** 2. Things to do in the generic interface + +*** A settings configuration for Isabelle: add backwards + compatibility for older versions of Isabelle. + Waiting for Isabelle to provide some easy version + checking. + +*** B Cleanup display during settings processing. + +*** A fix display anomaly for Isar output with shrink windows: + display splits window unexpectedly. + +*** B document and simplify proof-script-span-context-menu-extensions + +*** C Add output highlighting to minibuffer in proof-shell-message. + (Quite tricky to get text properties onto text in minibuffer...) + +*** X A more flexible way of choosing which instance of PG we want, + allowing matches on the buffer before choosing the mode function. + +*** D Isabelle PG: Non-blocking for .thy loading from .ML files. + +*** B Generic adjusting of pretty-printer line width (currently + implemented in several instances) + +*** D Make code robust against accidental buffer kills + by regenerating auxiliary buffers automatically. + +*** D Bugs with extents: + Sometimes probs if try to assert a whole file while one is + being processed: (proof-set-queue-start end) call in + proof-done-advancing finds that queue span is detached. + Code is now robust for this. But why detach anyway? + +*** C Extensions with semantic tokens + Look at the Semantic Navigator package. Implements persistent + database of tokens. + +*** B Documentation: + Check new doc for hiding; add doc for dependencies, tracing. + Moving spans; navigating through locked region. + Favourite menu. + +*** C Fix byte compilation + Problem with proof-ass macro mechanism -- gets expanded during compilation. + +*** B generalize from Isabelle's "atomic scripting" theory file mode + to allow other instances which do not allow incremental + processing of files in major or auxiliary file types. + E.g. twelf, ACL2, LambdaCLAM. + Also, add the atomic scripting handling for Isabelle/Isar. + +*** B Move over to new better designed parsing function mechanism. + +*** D ChangeLog generation still not right. + Probs: duplicated entries when runs several times in same day. + Suggested fix: use rcs2log to generate the entire log, just take + a sensible number of lines from it. + (Ideal would be to get until a given date) + +*** C Fix the doc makefiles to adapt the image flag in PG-adapting.tex + properly, for dvi/ps targets + +*** B Generalize electric terminator mode for other parsing mechanisms. + +*** B Add parameter for help function so HOL help works nicely + +*** D Make tags support in lego.el and coq.el a bit more generic. + Use customization option proof-tags-support. + +*** D Display functions: does auto-delete-windows work with + window-dedicated as it should? (I thought it would switch + between 2/3 bufs as appropriate?). + +*** C Clean up assert-until-point stuff: should have just one + function, as a subroutine of assert-next-command; and no bizarre + never-used arguments! + +*** B proof-shell-restart should clear response buffer (only noticed with + proof-tidy-response=nil) + +*** D Continue programme of making adaptation easier. + +*** D Fix up sources to conform to library header conventions + see (lispref)Library Headers. + +*** D Proof shell exit function -- could try sending an interrupt first + if the process is busy, just to be polite (and avoid the 10 second + wait before it gets killed). + +*** C make pretty printer line width altering generic. + Make a generic hook (or hook-constructing macro) to adjust + pretty printer line widths, a la LEGO. Maybe find a better + place to do this that in the proof-shell-insert-hook (should + be triggered by resize events). + +*** D X-Symbol: is there a function to input in the minibuffer using + a token language? + +*** D Investigate possible toolbar refresh problems. + Sometimes extra clicks *are* needed. Why? + +*** C Consider supporting imenu instead, or as well as, func-menu. + +*** C Improved configurability of command settings, etc. + We should let command settings, etc, be a special type + which can be one of three things: + + 'string -- send this as a command to assistant + 'function -- call this interactively to return either + 'string -- send this as a command + nil -- do nothing (function does work). + + This way we cover commands which need prompting for extra + args, as well as elisp functions which do whatever's necessary. + Then use a generic function "proof-invoke-function" or similar. + +*** C Usability enhancement: + Movement of point after assert/retract commands + - configure by default for one command/line. + - Add option for many commands per line. + - Maybe shell like behaviour with pressing return? + +*** C Usability enhancement: + - Fix proof-script-command-separator and + proof-one-command-per-line flag, document them. + +*** C Support an extended version of dynamic abbreviations, to work + for commands rather than words. Should behave a bit like a history + mechanism in shell buffer: use M-n M-p to scroll up and down + through previous and forthcoming (matching) commands. + +*** B TESTING. + - Add automatic testing mechanism to test user-level functions PG + - Test schedule for things to try with a new instantiation + +*** D Is there a way to make colours defined for x work in mswindows too? + + defface specs with (type x) seem to work fine with (type mswindows) too. + Hassle to duplicate, is there an easy way to cover both? + +*** C Improve proof-easy-config mechanism. + + Let it be redoable by initializing some of the variables to + default values to begin with(?). e.g. proof-script-next-entity-regexps. + Convention is that everything must be set in proof-easy-config body. + Use custom to set everything to its default value from proof-config, + before invoking the body. + +*** B Add a new configuration setting for matching proof commands + which have no undo effect --- should be treated like comments + for undo. Perhaps would be useful for Isabelle, HOL, at least, + although it's tricky to see how it would be completely *safe*. + [ See discussion with Pierre re Coq undo command categories ] + +*** C Implement proof-generic-find-and-forget + <...>-count-undos, to simplify prover-specific code. + Complete reengineering of *-count-undos and + *-find-and-forget at generic level + +*** D Display buffer clearing: response buffer is cleared + too often/eagerly, perhaps? The output find-theorems or + similar doesn't last beyond a single proof step. + The problem is that we want to erase irrelevant + output from the response buffer for the previous + proof step. Consider making output from invisible + command persistent. + See attempted patch in + etc/patches/fix-attempt-for-eager-cleaning.txt + +*** C Add to proof-config those variables created in proof-easy-config for + font lock and syntax entries. Use these instead of primitive + elisp in the other configs, too. + +*** C Improvements to customization mechanism: watch the use + of customize-set-variable, odd for users who think it + means they've changed a setting! + (currently: next-entity-regexps, proof-splash-settings for Isabelle). + +*** C Add improvements to script movement in electric terminator mode. + Some commented regions in code. E.g. automatic newline/space after + C-c C-BS. + +*** C Make proof-{script,shell,goals,resp}-font-lock-keywords the + default way of setting font-lock-keywords, removing from + proof-easy-config and changing each supported prover instance. + +*** D Settings mechanism could be generalised for non-persistent settings + + local settings: + E.g. Coq has some settings which are local: "Focus" which + it doesn't make sense to save between sessions or issue + at the start of the session. + + Ideal would be to specify context when local settings are + relevant, as a predicate. + +*** D Modify response display routine a bit to center around recent output, + or display top, for long output. Makes better sense for big + screen-fulls, perhaps? Or maybe display top with an itimer to + move to the bottom after a couple of seconds delay, would be a + nice effect. + +*** D Scheme to detect type of buffer and choose between possible modes. + Help select Isar over Isa, maybe sml over HOL etc? + +*** D Fix the sentinel infinite loop bug which occurs in some cases + when proof shell startup fails. Same message is printed over + and over. Infinite in GNU Emacs. Why? See note at + end of proof-shell. [2hrs] + + +*** D See if there is a way of postponing func-menu loading. + +*** D Quit timeout enhancement: instead of killing immediately after + timeout, could give a message "not responding, kill immediately?" + +*** D Consider proof-generic-goal-hyp function, for proof by + pointing support. Based on `proof-shell-goal-regexp' which + I accidently introduced at one point. + +*** D Make code robust against accidental deletion of response/goals + buffer. Add functions proof-get-or-create-{response,goals}-buffer. + [30 mins] + +*** D proof-script-next-entity-regexps: + "However, it does not parse strings, comments, or parentheses." + Actually we could improve the generic code to ignore + headings which buffer-syntactic-context suggests are inside + comments or strings. + +*** D Change the name of "automatic multiple files" to something + more comprehensible. + +*** D Strange problem when running in tty mode: c-c c-RET seems to be + impossible to type. Consider binding C-c RET instead when + running on a console. + +*** D Tidy up library-loading and dependencies. (Probably do + this at the same time as organizing for the XEmacs + packaging mechanism) + +*** D Make compile should give error if any elisp compile fails. + +*** D Check support for proof-guess-command-line, new generic setting + added by Patrick. Don't know if anyone can use it, actually. + +*** D Usability enhancement: + - Fix asymmetry between "doing" and "undoing": doing will skip comments, + undoing will not. e.g. test case: (* tester *) intros; + +*** D Robustify and cleanup code by allowing functions in place of regexps + for proof-goal-command-regexp and proof-save-command-regexp. + New names: proof-goal-command-match, proof-save-command-match. + Then we can remove duplicity and simplify code. + +*** D BUGLETS: + - Response buffer doesn't scroll to display o/p (it does for debug msgs, + oddly). This might have been a 1998 design decision. + Maybe it should be a user option? + - XEmacs pg forces on font-lock, should it? + +*** D SMALL DELTAS: + - Consider setting proof-mode-for-script automatically? + Is it ever needed in the shell before the script mode has + been entered? + - In case active terminator leads to an error, delete it again? + (problem synchronizing) + - Improvements to script navigation commands. Would like some + uniformity with proof-find-next-terminator, and a better + implementation. Maybe we have four commands: find command start, + command end, and move to next command/previous command. + +*** D Make completion more generic. For Isabelle and Lego, we can build a + completion table by querying the process, which is better than + messing with tags. + +*** D outline configuration should be generic (or else documented for + each prover separately, since not guaranteed to work for all). + +*** D Check matching code carefully, in view of bug reported (now fixed) + for Isabelle. + Examine syntax tables for all instances, and whether + word matching is based on whitespace constituents or non-word + constituents. [6 hrs] + +*** D Implement proof-auto-retract idea. [4hrs] + +*** D da: Suggested improvement to interface for included files: + Currently have two cases: processing a single file, and + retracting which updates the included file list arbitrarily + (but assumes that only removals are made). A simpler and + more general interface would be to just have the second + case, and automatically find removed files and added files + between two versions of proof-included-files-list and + unlock or lock buffers appropriately. We could provide + a useful default function based on three regexps: + retract-file-regexp, add-file-regexp, clear-filelist-regexp. + Master regexp process-file-regexp would match all of + these cases. Could be multiple matches of the three above + within a single process-file-regexp to avoid processing + lots of urgent messages. (3h) + +*** D da: goal-hyp: this should be more generic. At the moment, there are + generic variables which are only used in the specific code: + proof-shell-goal-regexp and proof-shell-assumption-regexp. + This is confusing. I suggest making lego-goal-hyp the + default behaviour for proof-goal-hyp-fn a hook function. + That will work for Isabelle too. (15 mins) + +*** D proof-goal-command-regexp: the syntax of Coq spoils the + uniform use of a regexp to match a goal (since it allows + goals to begin Definition ...). Nonetheless, it would be + for this not to mean that everyone else needs to set + proof-goal-command-p. Perhaps some crucial regexps can + be used via proof-string-match-p which would allow a + function to be invoked instead? (Cf font lock). + Or via a new generic mechanism for matching or invoking a fn. + +*** D ROBUSTness: deal gracefully with possibility that goals buffer is + killed during session. (2h) + +*** D Add support to filter out unwanted noise from the prover by setting + up a regular expression proof-shell-noise-regexp [2hr] + +*** D support for templates e.g., in LEGO it would be nice if, by default, + fresh buffers corrsponding to file foo.l would automatically insert + "Module foo;" Probably by using a generic Emacs package. [2hr] + +*** D Review and prune "FIXME notes" which are notes about ongoing fixes + or sometimes things to do. [6hr] + +*** D Write proof-define-derived-mode which automatically adds a + call back hook somehow corresponding to our "proof-config-done" + mess. Propose this to maintainer of derived.el. (1.5hrs) + +*** D Improve proof-goal-command and proof-save-command: + `proof-goal-command' should be more flexible and support a + placeholder for the name and the actual goal. In LEGO, we have + Goal foo : absurd; + ... + Save foo; + Perhaps functions at the generic level to make suitable + values for the hook, e.g., + + (setq proof-goal-command (proof-prompt-named-goal "Goal %s :" "%s;")) + +*** D Multiple files: handle failures in reading ancestors. + +*** D Provide a sensible default frame/buffer layout (4h) + +*** D Implement mouse drag-and-drop support for selecting subterms in the + goals buffer and copying them in a script buffer. This could be + implemented by defining button2 in the response buffer and setting + button2up in script buffers. (1h) + +*** D Add support to proof.el for *not* setting variables for + commands which aren't supported by a prover. For example, + in Isabelle there is no such thing as killing a goal. + +*** D proof-find-next-terminator is too slow when it needs to parse + a long buffer. Generally a performance problem with + proof-segment-up-to. + + +*** D Implement proof-find-previous-terminator and bind it to C-c C-a + (45min) + +*** D Implement a function to undo to the previous goal. + +*** D Remove duplication of variables e.g., proof-prog-name and + lego-prog-name for Coq and Lego. (1h) + +*** D More flexible help configuration is needed. HOL has some nice + on-line help but no way in PG to help by library. Perhaps + a help browser is needed? At least, optional arg to help command. + [patch ready and waiting to go in] + +*** X Display management is much better than it was, but perhaps + not quite as good as it could be. It might be nice to + display both the goals and response buffer occasionally + (even with window-dedicated disabled). + e.g. when proof-shell-erase-response-flag is non-nil + and the goals buffer is updated: might like to still + see what was in the response buffer. + +*** X Oddities: + Response buffer doesn't get cleared after completion + of a proof followed by retraction of whole file. + On other cases of retraction, it does. + Perhaps retraction should set the flag to ensure + it's cleared. + +*** X Making undoing better. + Rather than calculating an undo command each time an undo command + is needed, another idea would be to keep the undo command in the + span. Then when we amalgamate spans we can construct new undo + commands. When we come to issue an undo, we either need to do + each undo step in turn in reverse, just the final one, or perhaps + some proof-assistant dependent filtering/modification of the + set. At the moment, though, PG is rather keen on issuing just + one command to forget to some specific place in the script. + [Maybe a design principle is that spans should coincide with + undoable regions] + + + +** 3. Things to do for the documentation + +*** A Doc new bits: proof-next-error + +*** A Doc new bits: font lock keywords, filename %e, %r. + Added proof-{script,shell,goals,resp}-font-lock-keywords. + Presently used only in proof-easy-config, will put into other + mechanism + +*** A Doc new bits: win32 support + +*** A Doc new bits: settings mechanism via defpacustom + +*** C Update front page image + - Should include ??? logo to represent other provers + +*** B Manual improvements before techreport publishing (see notes at end also): + - Mention configuring function menus, outline. + - Consider splitting up chapter 9? + - document mouse functions, proof-cd, process quit timeout, + X-Symbol, prog-name-guess, new menu functions for display. + - general tips on what to do when things go wrong: try + interrupt, restart, finally exit proof assistant. + - improvements after feedback from users. + - add screenshots? + - add more index entries + +*** B Add something to better document two-buffer versus three-buffer + interaction modes, and the use of proof-window-dedicated to + trigger three buffer mode. + +*** C Documentation in pdf format: need to fix inclusion of image + problem. + +*** D Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General + info file into a good place. + +*** D texi-docstring-magic: first time deffn's, etc, are added, whitespace + after magic comment is left. + +*** B Doc enhancement: explain conditions for switching buffers and auto + switching of scripting buffers. (See doc of + proof-auto-action-when-switching-scripting) + + + +** 4. Emacs issues + +*** GNU Emacs issues + +**** A Improve support for Emacs 21. + X-symbol 4.X fixup for provers other than Isabelle. + +**** B Consider replacing buffer-substring -> buffer-substring-no-properties + Text properties are passed around in spans, probably needlessly. + (not the same in XEmacs?) + +**** C Changed implementation of overlays inside Emacs itself. We seem to + need 'priority property of overlays for queue and locked to make + sure the colours show through. Even then highlighting is strange, + and background face spoils the others. Transparent? + Same priority: we get mouse highlighting but no face property. + Higher priority: we get blanking as mouse highlighting. Yuk. + ACTION: check Emacs Lispref for hints. Maybe ask on newsgroup. + +**** X `proof-zap-commas-region' does not work for Emacs 20.4 on + lego/example.l . On *initially* fontifying the buffer, + commas are not zapped. However, when entering text (on + a particular line), commata are zapped correctly. (4h) + +*** XEmacs issues + +**** C Ask for easy-menu to support :visible keyword + Very useful option of GNU Emacs easy menu to remove items + from menu altogether, dynamically. (Or at least, fairly + dynamically. Fully dynamically would be guitrocity). + + + + +** 5. Things to do for subterm markup / proof-by-pointing + +*** B Unify proof-insert-pbp-command and proof-shell-insert-loopback-cmd. + Add some debugging messages in proof-done-advancing to indicate + Maybe pbp should be a new class of "'pbpadvancing" since we don't + want to allow the flexible queue manipulation here? Think on it. + +*** B Change proof by pointing (pbp) stuff into proofstate buffer stuff. + Outsource actual pbp/goals functionality + (separate pbp annotations from other annotations). + Rename pbp-mode to response-mode or goals-mode (which doesn't + support any actual proof-by-pointing), Make a file + proof-goals.el. [4 hrs] + +*** C Extend balloon-help (e.g. show pbp command) + +*** C Fixing up errors caused by pbp-generated commands; currently, script + management unwisely assumes that pbp commands cannot fail. + da: Is this still true? It looks fine to me. I think "failure" + should mean generates an error. With LEGO pbp, it uses "Try" + tactic which always succeeds, whether or not something gets done. + +*** C In case of pbp failure (real failure), we might keep a flag + to indicate that the next pbp command should delete the + previous pbp command's insertion into the buffer, to replace + it with another one. + +*** X pbp code doesn't quite accord with the tech report; in particular it + decodes annotations eagerly. Lazily would be faster, and it's what + the tech report claims --- djs: probably not much faster, actually. + + + + + + +** 6. Things to do for Web Pages, Distribution + +*** C simplify editing of web pages by instead including files + with version numbers in them, at least for development version. + Can also use the link "-latest". + +*** C Remove fileshow urls in html + +*** D Add an animation, showing proof replay. + +*** C Wanted for links: something to UITP. Are there any pages? + +*** C Validate pages. + Current failures for HTML 4.0 to do with CGI-style arguments with "&", + this is a problem with PHP3 really. + +*** X Restructure so that page titles are different to help + browsing. (Move links_arr from header.html somewhere new, + and set $pg_title appropriately before head.html is included). + +*** X Add some one-stop-shop pages. Ask permission to redistribute + packages for PAs. Maybe do Windows and Linux versions. + + + + +** 7. Future improvements to take advantage of newer Emacsen + +*** X XEmacs 21.2 compatibility/improvements +**** Accelerators for PG menus? (how to customize?) +**** Use one-shot-hook for splash display + +*** X GNU and XEmacs improvements +**** Indirect Buffers + Maybe a cunning way to implement the response buffer and goals + buffer, since they're basically variants on displaying fragments of + the shell buffer output. Appears in XEmacs 21.2, GNU 20.5 + + + + + + +** 8. Bugs in other software beyond our control + +*** A Nasty bug in Emacs 21.{1,2} triggered by + proof-shell-dont-show-annotations. Report this. + +*** X Code for find-alternate-file has annoying habit of nullifying + buffer-file-name before kill functions are called, on a buffer + named ** lose **. This means PG has to keep a copy of the + buffer file name to handle proof-included-files-list nicely. + Would be better if (X)Emacs code didn't do this. + +*** X useful if call-process would keep last error state + (primarily for exec-to-string, in case of errors) + +*** X Odd behaviour of font-lock in script buffers when long strings +contain lines with stuff that looks lisp-ish. e.g. "(asd . ads)" + +*** X oddity: startup delay when running XEmacs remotely and local display +is 8 bit. Suspect an XEmacs issue to do with face allocations. Also +huge delay in buffers for Isabelle mode which try to highlight binders +(removed because they appear inside strings anyway) + +*** X spurious byte comp warning in XEmacs 21.1.4: + While compiling proof-x-symbol-encode-shell-input: + ** buffer-substring called with 3 args, but requires 0-3 + for this code: + (prog1 (buffer-substring) + (kill-buffer (current-buffer)) + +*** X Error with pdftexinfo (hacked version of teTeX pre-release, 1.0.6). +Gives problem with @value{blah} inside @pdfurl. May be absent from +pdftexinfo.tex, but that version doesn't seem to generate web links? + +*** (/usr/share/texmf.local/pdftex/texinfo/pdftexinfo.tex +Loading texinfo [version 1999-09-25.10]: Basics, pdf, +(/usr/share/texmf/pdftex/plain/misc/pdfcolor.tex) fonts, page headings, +tables, conditionals, indexing, sectioning, toc, environments, defuns, macros, +cross references, (/usr/share/texmf/tex/plain/dvips/epsf.tex) localization, +and turning on texinfo input format.)) (ProofGeneral.aux) [1[/usr/share/texmf/d +vips/config/pdftex.map][/usr/share/texmf.local/dvips/config/dalucida.map][/usr/ +share/texmf.local/dvips/adobe/agaramon/pad.map][/usr/share/texmf.local/dvips/co +nfig/wp1.map][/usr/share/texmf.local/dvips/config/mscore.map][/usr/share/texmf. +local/dvips/config/barbedor-ttf.map][/usr/share/texmf.local/dvips/config/goodtt +.map]] [2] (Preface) +! Undefined control sequence. +@indexbreaks ->@catcode `@-=@active @let - + @realdash +@value ...ode `@-=12 @catcode `@_=12 @indexbreaks + @let _@normalunderscore @v... +<argument> @value + {URLpghome} +@pdfurl ...r{/Subtype /Link /A << /S /URI /URI (#1 + ) >>}@endgroup +@douref ...->@begingroup @unsepspaces @pdfurl {#1} + @setbox 0 = @hbox {@ignore... +l.264 @uref{@value{URLpghome}} + . Visit this page for +? x +<cmtt10.pfb><cmsy10.pfb><8r.enc><bsfr8a.pfb><bsfc8a.pfb> +Output written on ProofGeneral.pdf (2 pages, 54702 bytes). + + + + + + + + + + + +** 9. New Stable Version Release checklist + + +*** 0. Make all files have same CVS branch with cvs commit -f +*** 1. Tests: multiple file test suites for LEGO, Isabelle; other egs +*** 2. Check case with GNU Emacs +*** 3. Check case with compiled code, for XEmacs only. + (Wait for error reports for GNU Emacs) + Even if the code is faulty afterwards, compiling is + worthwhile just because it shows up bugs in unbound variables, etc. +*** 4. Dates and versions updated. + Check README, doc/ProofGeneral.texi, html/download.html, others. +*** 5. ProofGeneral.texi docstring magic is up-to-date: cd doc; make magic +*** 6. Update Emacs and prover versions in texi, html/ +*** 7. Check web page references from other places. +*** 8. Validate web pages if they're changed much. +*** 9. Update and distribute etc/announce. +*** 10. Message to PG mailing list. + + + + + + +** 10. Things to do for Proof General Project + + +*** A Journal paper on design and development of Proof General. +*** A Grant proposal for Proof General Kit. +*** A Informatics research reports from latest docs. +*** A Small project grant from LFCS for summer student (2003) + +*** C PG CDROM: CDROM with PG and other theorem provers + Complete read-to-go distributions. Could make up from TYPES 2002 + summer school systems to make sure of a consistent set of progs? + +*** B Find new people to help advance and develop Proof General. + Getting more instances is a good way. Also encouraging feedback. + Hear stories of bugs by word-of-mouth, they don't get reported often + enough. + +*** A PG projects + +*** B PG auxiliary contributions + - span library + +*** A PG research directions: + - protocols for interactive proof + - configuration management / dependency organization + - ideas about proof engineering cf software engineering + - research on ways of conducting a formalization, cf + ways of writing a program. Common idioms that PG could + help with. + + +================================================================= + +List of things postponed from PG 3.4: need to be merged above + +*** Stefan Monnier's big patch (Coq stuff, imenu, other) + +*** Isar tracing error: (error/warning) Error in process filter: (error Nesting too deep for parser) + +*** Coq pbp focussing --- does this part work at least? Test case. + +*** Christophe's changes suggested for handling x-sym / highlighting. + +*** Comment at the end for Isabelle theory files!!!! + +*** X-Symbol 4.4 backwards compatibility for Coq and friends. + +*** Check: does proof-follow-mode have any effect??? + Consider removal to simplify it? + +*** Fix-up show/hide for nested proofs. (Wierdness with + cursor jumping as well) + +*** Cleanup undo behaviour to cope with new Coq mechanism. + + Is the simplified mechanism better for other provers too, or does the + split still apply? Probably best to leave Isar as-is and have + proof-nesting-depth left as experimental. + +*** proof-nesting-depth: + This needs to be fixed up in count undos, find-and-forget. + +*** Generic versions of count undos and find-and-forget generic. + +*** Keybindings on menus: many missing in GNU Emacs. + Also strange things happen with docstrings for macro-generated + functions. (C-h C-c C-p gives message "can't find docstring for + proof-prf" at one point, then later finds it?!) |