Fixed small bugs in indentation.

3 files changed, 104 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 78b72bdc..bceeca3d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -92,6 +92,14 @@
 *** Some keyboard shortcuts are now available in goals buffer
     C-c C-a C-<c,p,o,b,a> are now available in goal buffer.
 
+*** Experimental storing buffer
+    To store the content of response or goals buffer in a dedicated
+    persistent buffer (for later use), use Coq/Store response or
+    Coq/Store goal.
+
+*** bug fixes
+    (Three panes mode, indentation).
+
 ** Notable internal changes
 
 *** Altered prover configuration settings (internal)
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index bfab8dfc..3a7b1d42 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -268,6 +268,31 @@ The point is put exactly before first non comment letter of the command."
           (nd (or (coq-find-command-end-forward) (- (point-max) 1)))) ; idem?
       (if st (buffer-substring st (+ nd 1))))))
 
+(defun coq-ident-line-number (pt)
+ (save-excursion
+   (goto-char pt)
+   (if (= 0 (current-column)) (+ (line-number pt) 1)
+     (line-number pt))
+   )
+ )
+
+(defun same-line (pt pt2)
+ (or (= (coq-ident-line-number pt) (coq-ident-line-number pt2))))
+
+(defun coq-commands-at-line ()
+ "Return the string of each command at current line.."
+ (save-excursion
+   (back-to-indentation)
+   (let ((initpoint (point))
+         res)
+     (while (same-line (point) initpoint)
+       (setq res (cons (coq-command-at-point) res))
+       (if (coq-find-command-end-forward)
+           (ignore-errors (forward-char 1) (coq-find-real-start))
+         (goto-char (- (point-max) 1))))
+     res
+     )))
+
 (defun coq-indent-only-spaces-on-line ()
   "Non-nil if there only spaces (or nothing) on the current line after point.
 Moves point to first non space char if present, to the end of line otherwise."
@@ -483,6 +508,35 @@ Returns point if found."
       )))
 
 
+(defun coq-save-count (l)
+ (if (eq l nil) 0
+   (+ (if (coq-save-command-p nil (car l)) 1 0)
+       (coq-save-count (cdr l)))))
+
+(defun coq-goal-count (l)
+ (if (eq l nil) 0
+   (+ (if (coq-indent-goal-command-p (car l)) 1 0)
+       (coq-goal-count (cdr l)))))
+
+(defun coq-proof-count (l)
+ (if (eq l nil) 0
+   (+ (if (proof-string-match "\\<Proof\\>" (car l)) 1 0)
+       (coq-proof-count (cdr l)))))
+
+(defun coq-goal-save-diff (l)
+ (- (coq-goal-count l) (coq-save-count l)))
+
+(defun coq-goal-save-diff-maybe-proof (l)
+  (let ((proofs (coq-proof-count l))
+        (goals (coq-goal-count l)))
+    (if (= goals 0) (- (if (<= proofs 0) 0 1) (coq-save-count l))
+      (- goals (coq-save-count l))
+      )
+    )
+)
+
+
+
 (defun coq-indent-command-offset (kind prevcol prevpoint)
   "Returns the indentation offset of the current line. This function indents a *command* line (the first line of a command). Use `coq-indent-expr-offset' to indent a line belonging to an expression."
   (cond
@@ -491,18 +545,26 @@ Returns point if found."
 
    ;; we are at an end command -> one ident left
    ;; FIX: we should count the number of closing item on the line
-   ((coq-save-command-p nil (or (coq-command-at-point) ""))
+   (;(coq-save-command-p nil (or (coq-command-at-point) ""))
+    (and (< (coq-goal-save-diff-maybe-proof (coq-commands-at-line)) 0)
+         (save-excursion (goto-char prevpoint)
+                         (<= (coq-goal-save-diff-maybe-proof (coq-commands-at-line)) 0))
+         )
     (- proof-indent))
 
 
    ;; previous command is a goal command -> one indent right
    ;; carreful: this line moves the point
-   ((and (goto-char prevpoint)
+   ((and (>= (coq-goal-save-diff-maybe-proof (coq-commands-at-line)) 0)
+         (goto-char prevpoint)
          (or (and;;"Proof ..." is a proof start (but not really a goal command)
               ;;  unless followed by a term (catch by coq-save-command-p above
               (proof-looking-at-safe "\\<Proof\\>")
-              (not (coq-save-command-p nil (coq-command-at-point))))
-             (coq-indent-goal-command-p (coq-command-at-point))
+;              (not (coq-save-command-p nil (coq-command-at-point)))
+              (<= (coq-goal-save-diff-maybe-proof (coq-commands-at-line)) 0)
+              )
+;             (coq-indent-goal-command-p (coq-command-at-point))
+             (> (coq-goal-save-diff-maybe-proof (coq-commands-at-line)) 0)
              ))
     proof-indent)
 
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
new file mode 100644
index 00000000..b06ae922
--- /dev/null
+++ b/coq/ex/indent.v
@@ -0,0 +1,30 @@
+Require Import Arith.
+
+
+Function div2 (n : nat) {struct n}: nat :=
+  match n with
+    | 0 => 0
+    | 1 => 0
+    | S (S n') => S (div2 n')
+  end.
+
+
+Module toto.
+  Lemma l1: forall n:nat, n = n. 
+    toto.
+  Qed.
+  Lemma l2: forall n:nat, n = n. 
+  toto. Qed.
+  Lemma l3: forall n:nat, n <= n. intro. Qed.
+  Lemma l4: forall n:nat, n <= n. Proof. intro. Qed.
+  Lemma l5 : forall n:nat, n <= n.
+  Proof. intro.
+  Qed.
+  Lemma l6: forall n:nat, n = n. 
+    toto.
+    Lemma l7: forall n:nat, n = n. 
+      toto.
+    Qed.
+  Qed.
+End toto.
+