Renamed file

1 files changed, 263 insertions, 0 deletions

diff --git a/TODO.defunct b/TODO.defunct
new file mode 100644
index 00000000..4943e3d8
--- /dev/null
+++ b/TODO.defunct
@@ -0,0 +1,263 @@
+-*- 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.
+