blob: c9d5fd66826a20a3ac712a26600ffa5c8b7c7630 (
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
|
This is our brief list of planned things to do to Proof General.
See also the appenix "Plans and Ideas" in the manual.
Please send any suggestions, comments, or offers of help to
proofgen@dcs.ed.ac.uk. Thanks!
Plans for later 3.x versions
----------------------------
* Queue manipulation improvment: allow to extend or reduce
during processing, with fewer "Proof Process Busy"
messages.
* Isabelle PG: Non-blocking for .thy loading from .ML files.
* 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.
* Make an XEmacs package
* Fix known problems with 3.0 (see developers `todo')
Plans for even later versions
-----------------------------
* Implement "Atomic Command Sequence" idea, or something like
it. To allow more flexible understanding of undo behaviour
of proof assistants.
* Add completion of theorem names, choice of proof commands, etc.
* 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.
|
