From 59c8f587f0997a18acb531e19a22cd8b389e4cb1 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 6 Apr 2004 15:04:11 +0000 Subject: Added example count undos function (completely untested) --- ccc/ccc.el | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'ccc') diff --git a/ccc/ccc.el b/ccc/ccc.el index f7b55a03..b2dc68d7 100644 --- a/ccc/ccc.el +++ b/ccc/ccc.el @@ -41,6 +41,34 @@ proof-shell-init-cmd "" proof-shell-proof-completed-regexp "^Consistency proof successfully finished." proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" ;;; ??? + proof-count-undos-fn 'ccc-count-undos ) + +;; da: example of a possible count undos function -- replace upper case +;; strings by real stuff + +(defun ccc-count-undos (span) + "Count number of undos in a span, return the command needed to undo that far." + (let + ((count-ccc 0) + (count-casl 0) + casl) + (while span + (setq str (span-property span 'cmd)) + (if (proof-string-match "HOL-CASL GOAL COMMAND REGEXP" 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)))))) + (setq span (next-span span 'type))) + (format + "HOL-CASL UNDOS (%s); CCC-UNDOS (%s);" + count-cassl count-ccc))) + + (provide 'ccc) + + -- cgit v1.2.3