blob: a5936b05aec7a269fc04b7e9617138baf27aa63f (
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
|
Some test cases for Proof General.
==================================
8.12.98 INHIBIT VARIABLES
==========================
Test with proof-splash-inhibit=t
Test with proof-toolbar-inhibit=t
8.12.98 SCRIPTING FOR BUFFERS WITHOUT FILES.
=============================================
Switch to a fresh buffer FOO which doesn't visit a file.
Do M-x isa-mode RET.
Should succeed.
Try asserting commands, e.g. Goal "P-->P";
Switch to another fresh buffer BAR, turn on isa-mode.
Should succeed again.
Try asserting commands here, e.g. Goal "Q&Q --> Q";
Should give error "Cannot have more than one active scripting buffer".
Exit emacs. Should query whether we want to save these
scripting buffers (maybe XEmacs only).
|
