blob: 3efba2d0f1d13ada213e6047abfcf5915c4179b9 (
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
|
This is our brief list of planned things to do to Proof General.
Please send any suggestions, comments, or offers of help to
proofgen@dcs.ed.ac.uk. Thanks!
Plan of Changes for Proof General 2.2
--------------------------------------
* Fix bugs and improve code and documentation
Based on user feedback.
* Queue manipulation improvment: allow to extend or reduce
during processing, with fewer "Proof Process Busy"
messages.
* Font-lock based on annotations in proof assistant output.
Particularly: colouration for Isabelle variable names.
* x-symbol support integration.
* Isabelle PG: Non-blocking for .thy loading from .ML files.
(hopefully as happy side effect of queue improvement)
* Improve process handling 1
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.
MEDIUM TERM
-----------
* Add an example instantiation of Proof General
using no prover-specific extensions (perhaps for Isabelle)
LONGER TERM
-----------
* Add a browser mode for browsing script files
and/or theory data-structures in the prover.
* Add more per-prover functions: menus for tactics, etc.
* Improve process handling 2
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.
|