From bcf862425eaf541ca490fcd3f209f2cc938310b5 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 6 Oct 1999 11:17:22 +0000 Subject: updates --- todo | 204 +++++++++++++++++++++++++++++++------------------------------------ 1 file changed, 93 insertions(+), 111 deletions(-) diff --git a/todo b/todo index 1c839a98..5bdbf99f 100644 --- a/todo +++ b/todo @@ -45,62 +45,13 @@ A Pending work, in progress [da]: - investigate toolbar refresh problems . extra clicks are needed (?) - investigate of excessive processing for large proofs + (on my machine, I see about a 30% 70% worse case between Xemacs and smlnj + for the time_use_thy in src/HOL/Real/ROOT.ML) - investigate bug fix for vacuous locked regions - - document proof-mouse-track-insert (new name for proof-send-span, re-enabled), proof-toggle-scripting, new configuration options. + - document proof-mouse-track-insert (new name for proof-send-span, +re-enabled), proof-toggle-scripting, new configuration options. + proof-cd -B 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. - -B Fix colouring of response buffer, may be broken. The idea was - that the latest message would always be highlighted, I think. - -B Usability enhancement: remove stupid "I don't know what I should be doing" - errors and replace with something more informative. - -B Doc enhancement: explain conditions for switching buffers and auto - switching of scripting buffers. (See doc of - proof-auto-action-when-switching-scripting) - -D Multiple file improvements: add implicit -D Usability enhancement: - - Fix asymmetry between "doing" and "undoing": doing will skip comments, - undoing will not. e.g. test case: (* tester *) intros; - -C Usability enhancement: - - Fix proof-script-command-separator and proof-one-command-per-line flag, - document them. - -D Internal improvements for marking up proof assistant output. - We need a better mechanism for allowing "invisible" mark up - of assistant output based on annotations. Present code - allows proof-shell-leave-annotations-in-output=t to work - together with font-lock to do mark up. - Instead we need something more like what enriched-mode does - (although I've just tried it and I foound that copying with - the mouse ignores the text properties, but copying with the - keyboard copies them!). It uses a general library - format.el for reading and writing files in multiple formats. - This is not quite what we want for our purpose, but it might be a - closer approximation than using font lock and hiding the special - characters. - Maybe using x-symbol would give another approximation, too, although - I'm put off that because it's not so standardly a part of XEmacs yet. - Or maybe w3's code for HTML mark up could be borrowed. - -D Usability enhancement: - Enable toolbar in other PG buffers. Should switch to active - scripting buffer first if it is non current. - In fact, a sensible subset of scripting commands would - work from other buffers. - This suggestion is based on observation of a user's - confusion when the toolbar disappears from other PG buffers. - -X Compatibility enhancement: - - Consider sending comments to proof process after all. They might - contain special (e.g. LaTeX) directives or something. - Probably only worth considering if/when it becomes a problem. C Usability enhancement: Movement of point after assert/retract commands @@ -120,6 +71,8 @@ C Usability enhancement: Proof General itself should work out whether it's a retraction or advancement! +C Unify toolbar and menu functions. (1h) + B Web pages: improve screenshots section to include a slideshow, or at least, a series of pictures of PG in action. (3 hours) @@ -128,20 +81,22 @@ C Nicety enhancement: This needs some call backs or setting of variables examined by proof-done-{advancing,retracting} -D bug: outline mode when proof-strict-read-only is nil ought to - work, but there may be problems. +C Fix colouring of response buffer, may be broken. The idea was + that the latest message would always be highlighted, I think. -D bug: mentioned by Martin H. with Lego: "don't know what I should - be doing..." error when it shouldn't happen. - [this item is useless without a more detailed description] +C Usability enhancement: remove stupid "I don't know what I should be doing" + errors and replace with something more informative. -C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting - ELISP_DIRS somehow. +C Doc enhancement: explain conditions for switching buffers and auto + switching of scripting buffers. (See doc of + proof-auto-action-when-switching-scripting) -D Update logo to include new "???" prover badge (maybe it should be - "...") from graphics file elsewhere (da) +C Usability enhancement: + - Fix proof-script-command-separator and proof-one-command-per-line flag, + document them. -D Add etc/announce to web pages somewhere. +C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting + ELISP_DIRS somehow. B Improve relocatability of RPM package, and produce package for XEmacs which installs directly under ~/.xemacs/packages. @@ -154,12 +109,72 @@ C Check compilation okay, check on use of eval-and-compile. C Support for proof-guess-command-line, new generic setting added by Patrick. +D Update logo to include new "???" prover badge (maybe it should be + "...") from graphics file elsewhere (da) + +D Add etc/announce to web pages somewhere. + D Key binding and interface issues - Consider change for prefix argument for C-c C-u and C-c u, it's quite easy to accidently delete by pressing C-c C-u repeatedly. -D CVS repository issues. +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 Internal improvements for marking up proof assistant output. + We need a better mechanism for allowing "invisible" mark up + of assistant output based on annotations. Present code + allows proof-shell-leave-annotations-in-output=t to work + together with font-lock to do mark up. + Instead we need something more like what enriched-mode does + (although I've just tried it and I foound that copying with + the mouse ignores the text properties, but copying with the + keyboard copies them!). It uses a general library + format.el for reading and writing files in multiple formats. + This is not quite what we want for our purpose, but it might be a + closer approximation than using font lock and hiding the special + characters. + Maybe using x-symbol would give another approximation, too, although + I'm put off that because it's not so standardly a part of XEmacs yet. + Or maybe w3's code for HTML mark up could be borrowed. + +X Multiple file improvements: add automatic/implict handling of + multiple files, by retracting across file boundaries automatically + if there is no support from the proof assistant to do this. Idea is + that when we retract file B and loaded files list is A B C D E, + then C D E are retracted too (one by one). Retraction should + happen (before) first undo takes place in a buffer on the loaded + files list. Type theory proof assistants with a linear context + can be handled perfectly this way. + +X Usability enhancement: + Enable toolbar in other PG buffers. Should switch to active + scripting buffer first if it is non current. + In fact, a sensible subset of scripting commands would + work from other buffers. + This suggestion is based on observation of a user's + confusion when the toolbar disappears from other PG buffers. + +X Compatibility enhancement: + - Consider sending comments to proof process after all. They might + contain special (e.g. LaTeX) directives or something. + Probably only worth considering if/when it becomes a problem. + +X bug: outline mode when proof-strict-read-only is nil ought to + work, but there may be problems. + +X bug: mentioned by Martin H. with Lego: "don't know what I should + be doing..." error when it shouldn't happen. + [this item is useless without a more detailed description] + +X CVS repository issues. Where are obsolete 'fileattr' files generated from/maintained? Should junk these (which appear to say that tms is watching everything). @@ -262,7 +277,7 @@ C Improve indentation code and see why it's so slow (at least for Isabelle). Enable it for particular provers if it works okay (but must test in on large files). -C Regions in script buffer have nice "name" property and configurers +C Proofs in script buffer have nice "name" property and configurers have to set regexps carefully so that it works, but is it actually used anywhere? What's it good for? @@ -276,32 +291,17 @@ C 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;" (1h) -C Remove "FIXME notes" which are just notes I've put in about old - code in case something breaks (da, 10mins). +D Review "FIXME notes" which are notes about ongoing fixes or + sometimes things to do. -C Check on all FIXME notes. - -C automise testing procedures in etc/ +D automise testing procedures in etc/ C Write proof-define-derived-mode which automatically adds a - call back hook somehow. Propose this to maintainer of derived.el. - (1.5hrs) + call back hook somehow corresponding to our "proof-config-done" + mess. Propose this to maintainer of derived.el. (1.5hrs) C Toolbar icon for `proof-execute-minibuffer-cmd' (1.5hrs) -C Improve web pages after suggestions in doc/notes.txt - (da, 1.5hrs) - -C proof-issue-goal should refuse to work when a proof is in progress. - Similarly proof-issue-save should refuse to work when a proof - hasn't been completed! Algorithm: Search the last goal and check - length of span. (45min) - -C Bug in proof-retract-until-point when called twice in succession: - calls backward-char at beginning of buffer. (Should say no - locked region, or "nothing to retract"). Problems is that - there is a proof-locked-end, but it's at (point-min). (30min) - C Clean up proof-assert-until-point behaviour. Discussion results: 1. At the moment we get an odd error if it is run in the locked region. This is a bug. Should behave same @@ -331,45 +331,30 @@ C Improve proof-goal-command and proof-save-command: (setq proof-goal-command (proof-prompt-named-goal "Goal %s :" "%s;")) -C Cleanup handling of proof-terminal-string. At the moment some +X Cleanup handling of proof-terminal-string. At the moment some commands need to have the terminal string, some don't. da: I suggest removing proof-terminal-string altogether and adding back the semi-colons or fullstops at the specific level. It's not a big deal and would support other provers which may use a mixture of terminators, or no terminators at all. + [Trouble with this is that terminators are used for active + terminator mode, among several other things] -C Functions for next,previous input a la shell mode, but in proof - script buffer (3h, da). +X Functions for next,previous input a la shell mode, but in proof + script buffer (5h, da). -C User-level functions: - 1. add new version of undo-until-point which behaves analogously to - proof-assert-next-command. - 2. make version of proof-restart-script which will start or - restart the proof assistant as appropriate. (It's handy to have - a direct function to start the proof assistant). - (1hr, da) - -C Write test schedule for things to try out with a new instantiation +X Write test schedule for things to try out with a new instantiation of Proof General. -C Add skeleton instantiation files for a dummy prover "myassistant" to +X Add skeleton instantiation files for a dummy prover "myassistant" to make it easier to add support for new assistants -- looking at any of the existing modes is confusing because of the prover-specific stuff. Ideally it should work for one of the default provers as an impoverished example mode. - (2h, da will do for Isabelle) - -C file handling could be more robust; perhaps one should always cd to - the directory corresponding to the script buffer (currently only - done for the buffer which starts up the proof system). This could be - achieved with a hook which is not set by default. [Remember to add - user documentation] (30min) C Reengineer *-count-undos and *-find-and-forget at generic level (3h) -C Unify toolbar and menu functions. (1h) - C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's. Generic problem, really: maybe CRs should be stripped, and just first line of multiline urgent message displayed in minibuffer. @@ -385,9 +370,6 @@ D Perhaps goal..save sequences should be closed also by the appearance Will ACS idea handle this? -D Better support for adding a new prover: give error messages which - hint at what variable to set (see proof-issue-goal for example). - D Multiple files: handle failures in reading ancestors. D Provide a sensible default frame/buffer layout (4h) -- cgit v1.2.3