1 | Index: generic/proof-script.el |
---|
2 | =================================================================== |
---|
3 | RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-script.el,v |
---|
4 | retrieving revision 11.10 |
---|
5 | diff -B -b -c -r11.10 proof-script.el |
---|
6 | *** generic/proof-script.el 13 Apr 2011 11:12:49 -0000 11.10 |
---|
7 | --- generic/proof-script.el 18 Apr 2011 10:00:49 -0000 |
---|
8 | *************** |
---|
9 | *** 1203,1210 **** |
---|
10 | (unless (eq proof-buffer-type 'script) |
---|
11 | (error "Must be running in a script buffer!")) |
---|
12 | |
---|
13 | - (proof-shell-ready-prover queuemode) ; fire up/check mode |
---|
14 | - |
---|
15 | (unless (equal (current-buffer) proof-script-buffer) |
---|
16 | |
---|
17 | ;; TODO: narrow the scope of this save-excursion. |
---|
18 | --- 1203,1208 ---- |
---|
19 | *************** |
---|
20 | *** 1237,1255 **** |
---|
21 | (assert (null proof-script-buffer) |
---|
22 | "Bug in proof-activate-scripting: deactivate failed.") |
---|
23 | |
---|
24 | ! ;; Set the active scripting buffer, and initialise regions |
---|
25 | |
---|
26 | (setq proof-script-buffer (current-buffer)) |
---|
27 | ! (if (proof-locked-region-empty-p) |
---|
28 | ! ;; Clear locked regions, unless buffer is "full". |
---|
29 | (proof-init-segmentation)) |
---|
30 | |
---|
31 | ;; Turn on the minor mode, make it show up. |
---|
32 | (setq proof-active-buffer-fake-minor-mode t) |
---|
33 | (force-mode-line-update) |
---|
34 | |
---|
35 | ! ;; Perhaps a good time to ask if the user wants to save some |
---|
36 | ! ;; buffers. Query unsaved proof script buffers, excluding active one. |
---|
37 | (if (and |
---|
38 | proof-query-file-save-when-activating-scripting |
---|
39 | (not nosaves)) |
---|
40 | --- 1235,1254 ---- |
---|
41 | (assert (null proof-script-buffer) |
---|
42 | "Bug in proof-activate-scripting: deactivate failed.") |
---|
43 | |
---|
44 | ! ;; Fire up the prover (or check it's going the right way). |
---|
45 | ! (proof-shell-ready-prover queuemode) |
---|
46 | |
---|
47 | + ;; Set the active scripting buffer, and initialise regions |
---|
48 | (setq proof-script-buffer (current-buffer)) |
---|
49 | ! (if (proof-locked-region-empty-p) ; leave alone if non-empty |
---|
50 | (proof-init-segmentation)) |
---|
51 | |
---|
52 | ;; Turn on the minor mode, make it show up. |
---|
53 | (setq proof-active-buffer-fake-minor-mode t) |
---|
54 | (force-mode-line-update) |
---|
55 | |
---|
56 | ! ;; A good time to ask if the user wants to save some buffers |
---|
57 | ! ;; (idea being they may be included in imports at top of new buffer). |
---|
58 | (if (and |
---|
59 | proof-query-file-save-when-activating-scripting |
---|
60 | (not nosaves)) |
---|
61 | *************** |
---|
62 | *** 1273,1279 **** |
---|
63 | (proof-deactivate-scripting) ;; turn off again! |
---|
64 | ;; Give an error to prevent further actions. |
---|
65 | (error |
---|
66 | ! "Proof General: Scripting not activated because of error or interrupt"))))))) |
---|
67 | |
---|
68 | |
---|
69 | (defun proof-toggle-active-scripting (&optional arg) |
---|
70 | --- 1272,1278 ---- |
---|
71 | (proof-deactivate-scripting) ;; turn off again! |
---|
72 | ;; Give an error to prevent further actions. |
---|
73 | (error |
---|
74 | ! "Scripting not activated because of error or interrupt"))))))) |
---|
75 | |
---|
76 | |
---|
77 | (defun proof-toggle-active-scripting (&optional arg) |
---|