Moved handling of mixed undo into the CCC, so there is now just one undo() cmd.

1 files changed, 3 insertions, 46 deletions

diff --git a/ccc/ccc.el b/ccc/ccc.el
index d9d43aac..b675bf1f 100644
--- a/ccc/ccc.el
+++ b/ccc/ccc.el
@@ -19,11 +19,11 @@
  proof-terminal-char             ?\;
  proof-script-comment-start      "(*"
  proof-script-comment-end        "*)"
- proof-goal-command-regexp       "ccc \".*\";"
+ proof-goal-command-regexp       "\\(ccc\\|holcasl\\) \".*\";"
  proof-save-command-regexp       "^qeccc"
- proof-goal-with-hole-regexp     "ccc \"\\(\\(.*\\)\\)\"" 
+ proof-goal-with-hole-regexp     "\\(ccc\\|holcasl\\) \"\\(\\(.*\\)\\)\"" 
  proof-save-with-hole-regexp     "qeccc \"\\(\\(.*\\)\\)\""
- proof-non-undoables-regexp      nil ;; "undo\\|back"
+ proof-non-undoables-regexp      "undo\\|back"
  proof-goal-command              "ccc \"%s\";"
  proof-save-command              "qeccc \"%s\";"
  proof-kill-goal-command         "abort ();"
@@ -42,7 +42,6 @@
  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
 
  ;;
  ;; Some basic fontlocking and syntax table entries, as taken from the 
@@ -84,46 +83,4 @@
 )
 
 
-;; da: example of a possible count undos function -- replace upper case
-;; strings by real stuff
-;; cxl: TBD: to undo "holcasl", we need to issue "holcasl_abort()"
-
-;; > - in normal CCC proofs, we need undo (or undo_steps);
-;; > - once we entered HOL-CASL with a holcasl command (this is not a 
-;; > tactic), we use Isabelle's Goals.undo;
-;; > - but to undo the holcasl command itself, we use holcasl_abort();
-;; > If we do CCC's undo()  inside a HOL-CASL proof, we go back to the CCC 
-;; > step _before_ holcasl (precisely because holcasl is not a proper CCC 
-;; > tactic, and undo undoes the last applied tactic, just like in Isabelle).
-
-
-(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 str)
-    (while span
-      (setq str (span-property span 'cmd))
-      (cond ((eq (span-property span 'type) 'vanilla)
-	     (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
-     ((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 to outside "holcasl" (or just holcasl command)
-      (format "holcasl_abort(); undo_steps (%s);" count-ccc)))))
-
-(provide 'ccc)
-