From 4525eff5f0b03ed068020c9a8a8e9606b4643518 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 13 Apr 2004 11:38:28 +0000 Subject: Modified logic in ccc-count-undos --- thinking that "holcasl" command itself is not supposed to be counted. --- ccc/ccc.el | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'ccc') diff --git a/ccc/ccc.el b/ccc/ccc.el index 7af7555a..d997a757 100644 --- a/ccc/ccc.el +++ b/ccc/ccc.el @@ -82,24 +82,24 @@ casl) (while span (setq str (span-property span 'cmd)) - (if (proof-string-match "^holcasl .*" str) - (setq casl t)) (cond ((eq (span-property span 'type) 'vanilla) - (unless (proof-string-match proof-non-undoables-regexp str) - (if casl - (setq count-casl (+ 1 count-casl)) - (setq count-ccc (+ 1 count-ccc)))))) + (if (proof-string-match "^holcasl .*" str) + (setq casl t) + (unless (proof-string-match proof-non-undoables-regexp str) + (if casl + (setq count-casl (+ 1 count-casl)) + (setq count-ccc (+ 1 count-ccc))))))) (setq span (next-span span 'type))) (cond - ((and casl (> count-ccc 0)) - ;; we're undoing to outside "holcasl" - (format "holcasl_abort(); undo_steps (%s);" count-ccc)) - (casl + ((not casl) + ;; we're undoing within CCC + (format "undo_steps (%s);" count-ccc)) + ((and (> count-casl 0) (= count-ccc 0)) ;; we're undoing within HOL-CASL (format "funpow (%s) (Goals.undo) ();" count-casl)) - (t - ;; we're undoing within CCC - (format "undo_steps (%s);" count-ccc))))) + (t + ;; we're undoing to outside "holcasl" (or just holcasl command) + (format "holcasl_abort(); undo_steps (%s);" count-ccc))))) (provide 'ccc) -- cgit v1.2.3