diff options
Diffstat (limited to 'TODO.defunct')
| -rw-r--r-- | TODO.defunct | 263 |
1 files changed, 0 insertions, 263 deletions
diff --git a/TODO.defunct b/TODO.defunct deleted file mode 100644 index 4943e3d8..00000000 --- a/TODO.defunct +++ /dev/null @@ -1,263 +0,0 @@ --*- mode:outline -*- - -* Proof General Defunct List of Things to Do - -This is a list of things that fell out of todo. They'll -probably never be read again, let alone done... - - - -** Things to do in the generic interface - -*** X X-Symbol improvements: see if we can get support for - proof-xsym-extra-modes outside PG (just by loading proof-site). - Will be handy for Isabelle's .itex Isabelle-LaTeX files. - Then we can parameterise more of the xsym support, and - remove spurious settings of calculated stuff from - x-symbol-isa.el (see FIXME comments in v3.1 there). - -*** X X-Symbol improvement: turning it on/off seems to move point. - -*** X Why does dired get loaded when PG loads? (Can we speed - loading by avoiding a particular function?) - -*** X Process handling output. - Handling mixtures of urgent and non-urgent messages: - at the moment any non-urgent output *before* an urgent - message will not be displayed in the response buffer. - Accept this as a feature for now. - -*** X 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-fontify and - deleting the special characters. It would allow sgml-like - markupo in the future, too. - Or maybe w3's code for HTML mark up could be borrowed. - -*** X Idea: introduce a dynamic follow mode which follows - proof-locked-end rather than proof-queue-or-locked-end. - Would be annoying for interactive use though, point would - jump from under fingers (although no typing anyway, hardly - matters). Alternative is dynamic recenter mode to - keep end of locked region in buffer. - -*** X Improve goto button image [suggestion from Markus] - Is it possible to avoid the arrows to touch in the middle, - emphasizing the 'point' a bit more. The arrows look a bit outwards - bent, too. - -*** X Check compilation okay, check on use of eval-and-compile. - -*** X Difference in menubar appearance depending on whether X-Symbol - is loaded before Proof General or not. - -*** X Update logo to include new "???" prover badge - from graphics file elsewhere (da) - -*** X bug: outline mode when proof-strict-read-only is nil ought to - work, but there may be problems. - -*** X CVS repository issues. - Where are obsolete 'fileattr' files generated from/maintained? - Should junk these (which appear to say that tms is watching everything). - -*** X Fixup display problems. - The window dedicated stuff is a real pain and I've - spent ages inserting workarounds. Why do we want it?? - The latest problem is that with - (setq special-display-regexps - (cons "\\*Inferior .*-\\(goals\\|response\\)\\*" - special-display-regexps)) - I get the script buffer made into a dedicated buffer, - presumably because the wrong window is selected in - proof-display-and-keep-buffer? - [da: can't repeat this now, presume it has gone away?] - -*** X Add other image sources to images/ directory. - Add target to html/images to remove images generated from - the image directory. - -*** X splash screen: report XEmacs problem of not displaying transparent - gif properly. - -*** X Allow bib-cite style clicking on Load/Import commands to go - to file. - -*** X Images for splash screen: could add xpm files for logos - so that XEmacs displays transparent parts properly. - (Probably not worth effort of distributing more files). - -*** X Customization mechanism: is there a way to make saved settings - not be overwritten by setq's in the code? Need to think how - to do this, something like customize-set-variable-if-unchanged - Otherwise no so useful for people to use customize for - prover config settings (we'd need to shadow them all again for - each assistant for this to work smoothly). - Sure sign saving will fail is when you see "this option has - been changed outside customization buffer" - At the moment even setting config variables in a hook is tricky, - because proof-config-done is called before the hook variables for the - new mode are. Our new version of define-derived-mode needs - to address this. - -*** X Proofs in Isabelle scripts can be non-interactive. Non-interactive - proofs have only one command, effectively. It might be useful - to find a way to integrate these into Proof General nicely. - -*** X Code in proof.el assumes all characters with top bit set are special - instructions to Emacs. This is rather arrogant, and precludes proof - systems which utilize 8-bit character sets! Needs repair. (3h) - -*** X Span convenience functions for special 'type property. - Could put these in proof.el or somewhere. - -*** 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. - Wait until it's a problem for somebody. - [Trouble with this is that terminators are used for active - terminator mode, among several other things] - -*** X Functions for next,previous input a la shell mode, but in proof - script buffer (5h, da). - -*** (defsubst set-span-type-property (span val) - "Set type property of SPAN to VAL" - (set-span-property span 'type val)) - -*** (defsubst span-type-property (span) - "Get type property of SPAN" - (span-property span 'type)) - -*** etc. (1hr) - -*** X Read-only mode of extents sometimes gets in the way: for example, - if file changes on disk, can't reload it via usual functions. - Can this be improved? Always have to retract first, and that - leaves stuff around. - -*** X toolbar icons: Automatically generate reduced and - pressed/greyed-out versions from gimp xcf files. - (1 day's gimp hacking) - -*** X Proof General customization: how should it work? - Presently we have a bunch of variables in proof.el which are - set from a bunch of similarly named variables in <engine>-syntax.el. - Seems a bit daft: why not just have the customization in - one place, and settings hardwired in <engine>-syntax.el. - That way we can see which settings are part of instantiation of - proof.el, and which are part of cusomization for <engine>. - -*** X Moreover, I think it would be nice to change the architecture - to make customization for new provers much easier. - The standard use of 'define-derived-mode' could be invoked - automatically in proof-site, and we could easily get away from the - kludge of proof-config-done and friends. - (Compare this to the way font-lock works automatically for XEmacs - when the right variable name is set, but for GNU Emacs you have - to write something special). - The objection to doing this is based on the idea that we should use - an object-like inheritance mechanism to define the new modes. - But if this is forgone, it might even be possible to add - support for new assistants entirely via the customize mechanism, - without any knowledge of elisp apart from regular expressions! - [see proof-easy-config.el] - -*** X Support a history of proof commands, with a "redo" command to - redo undo-to-point or sequences of toolbar undo's. - -*** X Provers with sophisticated/configurable syntax should tell Emacs - about their syntax somehow, rather than trying to duplicate - specifications inside Emacs. - Maybe some particular ATerm format would help with this? - -*** X Comment support is not very generic: we don't support end-of-line - terminated comments. Is there any case where this might be - worthwhile? (2h to add it). - -*** X Make process handling smarter: because Emacs is single-threaded, - no process output can be dealt with when we are running some - command. This means that it would be safe to extend the - red region, by putting more commands on the queue. Also it would - be safe to implement a clever undo command which worked on the - red region: if there are commands waiting to be processed, we - could remove them from the queue. If there are no commands waiting, - we have to wait until something becomes blue to undo it by sending - a command to the process. - -*** X Ideas for efficiency improvements. Rather than repeatedly - re-parsing the buffer, we could parse the whole buffer *once* - and make adjustments after edits, like font-lock. We could - make an extent for every command, and set it to "blue", "red" - or "clear" as appropriate. (This would allow proofs to be - sent out-of-order to the proof process too, although perhaps - that's not so nice). - The function proof-segment-up-to could be made to cache its - result. - -*** X proof-mark-buffer-atomic marks the buffer as only containing - comments if the first ACS is a goal-save span. This is however not a - problem for LEGO and Isabelle. (30 min) - -*** X Add support for XEmacs 21 packaging. Make suitable updates available - on web page, and make RPM put things in the right place so no .emacs - file may need editing(?). [2 days] - -*** X The narrowing issue - Code uses (point-min) and (point-max) everywhere. - Most primitive functions give error if given arguments outside - a restriction. However, most places these are used in PG we really - mean the start or end of the buffer (e.g. when parsing). - The only way to fix this seems to be with messy - (save-restriction (widen) ... sequences. - -*** X Solaris bugs: font locking and button enabling. - - [Markus]: I can only produce this problem on Solaris, where we have - both a mule and non-mule version of xemacs-21.1.8. On my Linux box - at home there is no problem present (using xemacs-21.1.7-mule). - - Note that on the Solaris boxes the problem is already exhibited by - visiting a new/empty thy file: buttons are off and are not enabled - by typing new stuff. - - Moved down the list now, instead we disable button enablers on - Solaris. - -*** X Multiple session architecture (difficult) - - With some major re-engineering, PG could be made to work with multiple - provers at once, and multiple instances of the same prover. - - Ideas: - introduce "session" notion - - have list of current sessions in progress, - values of active scripting buffer and other per-session vars - for each one - - proof shell filter and other functions must automatically - switch context to correct session - - force everybody to use proof-easy-config macro, and set - <prover>-var automatically from <proof>-var there, - to get defaults for new sessions. - - - -** Things to do for Web Pages, Distribution - -*** X Convert to SSI only plus a meta-generation phase? - -*** X Add status bar messages to navigation bar - -*** X Get rid of footer() function. - |