isar-stack-to-indent: indent according to (current-column) of open cmd;

fixed isar-count-undos, isar-find-and-forget: proper handling of empty and diag commands;

1 files changed, 7 insertions, 3 deletions

diff --git a/isar/isar.el b/isar/isar.el
index 6b39686e..959af2ca 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -119,7 +119,7 @@
     (nth 1 (car stack)))
    (t (let ((col (save-excursion
 		   (goto-char (nth 1 (car stack)))
-		   (current-column))))
+		   (current-indentation))))
 	(if (and (eq (car (car stack)) ?p)
 		 (save-excursion (move-to-column (current-indentation))
 				 (looking-at isar-indent-enclose-regexp)))
@@ -436,7 +436,9 @@ Resulting output from Isabelle will be parsed by Proof General."
 (defconst isar-kill "kill;")
 
 (defun isar-undos (i)
-  (concat "undos_proof " (int-to-string i) ";"))
+  (if (> i 0)
+      (concat "undos_proof " (int-to-string i) ";")
+    proof-no-command))
 
 (defun isar-cannot-undo (cmd)
   (concat "cannot_undo \"" cmd "\";"))
@@ -447,7 +449,7 @@ Resulting output from Isabelle will be parsed by Proof General."
    (proof-ids-to-regexp (append isar-keywords-control isar-keywords-theory-end))))
 
 (defconst isar-undo-skip-regexp
-  (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-diag)))
+  (proof-anchor-regexp (concat ";\\|" (proof-ids-to-regexp isar-keywords-diag))))
 
 (defconst isar-undo-kill-regexp
   (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-theory-begin)))
@@ -490,6 +492,8 @@ Resulting output from Isabelle will be parsed by Proof General."
 	(setq ans isar-undo))
        ((proof-string-match isar-undo-fail-regexp str)
 	(setq ans (isar-cannot-undo str)))
+       ((proof-string-match isar-undo-skip-regexp str)
+	(setq ans proof-no-command))
        ((proof-string-match isar-undo-kill-regexp str)
 	(setq ans isar-kill))
        (t