TODO


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

This is our brief list of planned things to do to Proof General.

$Id$

See also the Proof General projects page on the web, under the
development section of the home page.  Also, see the appendix "Plans
and Ideas" in the manual, and for low-level detail, the file "todo" in
the developer release.

Please send any suggestions, comments, or offers of help to
proofgen@dcs.ed.ac.uk.  Thanks!


Plans for upcoming versions
---------------------------

* Support more proof assistants

* Add a browser mode for browsing script files 
  and/or theory data-structures in the prover.

* More flexible goals buffer mode to allow menus of
  common proof commands.

* Unified context (right-button) menu in and out of spans.
  Including paste option and other editing commands.

* Implement ideas in the Proof General White Paper. 
  (See the Development section of the web page for a link).

* A more flexible way of choosing which instance of PG we want,
  allowing matches on the buffer before choosing the mode function.

* Isabelle PG: Non-blocking for .thy loading from .ML files.

* Generic adjusting of pretty-printer line width (currently implemented
  in several instances)

* Queue manipulation improvement: allow to extend or reduce
  during processing, with fewer "Proof Process Busy" messages.  

* Improve process handling: disable interrupts and/or catch errors at
  crucial points in code so that C-g can safely be used during script 
  processing.  Handle deleted buffers smoothly.

* Implement "Atomic Command Sequence" idea, or something like
  it.  To allow more flexible understanding of undo behaviour
  of proof assistants.  Alternative is to base markup of 
  undoable regions on proof assistant output or messages.

* Make an XEmacs package