proof-indent-commands-regexp: use proof-no-regexp;

isar-global-save-command-p: more robust wrt. empty prev span (malformed!?);
isar-preprocessing: fixed terminator regexp;

1 files changed, 17 insertions, 26 deletions

diff --git a/isar/isar.el b/isar/isar.el
index ca40baa8..4f6da0ae 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -215,7 +215,7 @@
    proof-goal-command-regexp    isar-goal-command-regexp
    proof-goal-with-hole-regexp  isar-goal-with-hole-regexp
    proof-save-with-hole-regexp  isar-save-with-hole-regexp
-   proof-indent-commands-regexp	"$^"
+   proof-indent-commands-regexp	proof-no-regexp
    ;; proof engine commands
    proof-showproof-command	"pr"
    proof-goal-command		"lemma \"%s\";"
@@ -298,11 +298,6 @@
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
    proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
 
-   ;; Tested values of proof-shell-eager-annotation-start: 
-   ;; "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading"
-   ;; "^---\\|^\\[opening "
-   ;; could be last bracket on end of line, or with ### and ***.
-
    ;; Dirty hack to allow font-locking for output based on hidden
    ;; annotations, see isar-output-font-lock-keywords-1
    proof-shell-leave-annotations-in-output t
@@ -462,24 +457,20 @@ proof-shell-retract-files-regexp."
   (or
    (string-match isar-global-save-command-regexp str)
    (let ((ans nil) (lev 0) cmd)
-     (while (and span (not ans))
-       (setq span (prev-span span 'type))
-       ;; FIXME da: bug was here -- there may be no previous span!!
-       (if span				; da: added, don't know if right
-	   (progn			; da: added, don't know if right
-	     (setq cmd (span-property span 'cmd))
-	     (cond
-	      ;; comment: skip
-	      ((eq (span-property span 'type) 'comment))
-	      ;; local qed: enter block
-	      ((proof-string-match isar-save-command-regexp cmd)
-	       (setq lev (+ lev 1)))
-	      ;; local goal: leave block, or done
-	      ((proof-string-match isar-local-goal-command-regexp cmd)
-	       (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no)))
-	      ;; global goal: done
-	      ((proof-string-match isar-goal-command-regexp cmd)
-	       (setq ans 'yes))))))
+     (while (and (not ans) span (setq span (prev-span span 'type)))
+       (setq cmd (span-property span 'cmd))
+       (cond
+	;; comment: skip
+	((eq (span-property span 'type) 'comment))
+	;; local qed: enter block
+	((proof-string-match isar-save-command-regexp cmd)
+	 (setq lev (+ lev 1)))
+	;; local goal: leave block, or done
+	((proof-string-match isar-local-goal-command-regexp cmd)
+	 (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no)))
+	;; global goal: done
+	((proof-string-match isar-goal-command-regexp cmd)
+	 (setq ans 'yes))))
      (eq ans 'yes))))
 
 (defvar isar-current-goal 1
@@ -536,8 +527,8 @@ proof-shell-retract-files-regexp."
   "Insert sync markers - acts on variable STRING by dynamic scoping"
   (if (string-match isabelle-verbatim-regexp string)
       (setq string (match-string 1 string))
-    (unless (string-match ";[ \t]$" string) ; da: added this 
-      (setq string (concat string ";")))    ; da: added this
+    (unless (string-match ";[ \t]*\'" string)
+      (setq string (concat string ";")))
     (setq string (concat 
 		  "\\<^sync>" 
 		  (isar-shell-adjust-line-width)