aboutsummaryrefslogtreecommitdiffhomepage
path: root/todo.defunct
blob: 4943e3d8fd4d7dd3f0238024ef78d4255529d20c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
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.