diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-12 08:14:54 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-12 08:14:54 +0000 |
| commit | c27db1ac23f425d012a9d62b98a2d3f2354d309d (patch) | |
| tree | 1d52bdbd6c49ed53b686d68dd665063881491103 /generic | |
| parent | 9f223fa9ed8fbc437dd60b446e1e4f82e88a1096 (diff) | |
condition-case -> ignore-errors, comment.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 8d4c6ba6..e9c458a6 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -814,11 +814,10 @@ an error is signalled here." "Deactivate scripting without asking questions or raising errors. If the locked region is full, register the file as processed. Otherwise retract it. Errors are ignored" - (condition-case nil - (proof-deactivate-scripting - (proof-with-script-buffer - (if (proof-locked-region-full-p) 'process 'retract))) - ((error nil)))) + (ignore-errors + (proof-deactivate-scripting + (proof-with-script-buffer + (if (proof-locked-region-full-p) 'process 'retract))))) (defun proof-deactivate-scripting (&optional forcedaction) "Deactivate scripting for the active scripting buffer. @@ -1262,6 +1261,7 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; discarding the proof history. ;; Provers without flat history yet nested proofs (i.e. Coq) ;; need to keep a record of the undo count for nested goalsaves. + ;; FIXME: should also remove nested 'idiom spans. (setq lev 1) (setq nestedundos 0) (while (and gspan (> lev 0)) |