Fix #646. Indentation of function arguments.

ProofGeneral · Mar 25, 2022 · 58adaea · 58adaea
1 parent f34a493
commit 58adaea
Show file tree

Hide file tree

Showing 6 changed files with 220 additions and 23 deletions.
diff --git a/ci/test-indent/indent-equations.v b/ci/test-indent/indent-equations.v
@@ -10,6 +10,13 @@ Module Equations.
     neg true := false ;
     neg false := true.
 
+  Equations neg' (b : bool) : bool :=
+    neg' true
+    :=
+      false ;
+    neg' false :=
+      true.
+
   Lemma neg_inv : forall b, neg (neg b) = b.
   Proof.
     intros b.
@@ -41,6 +48,16 @@ Module Equations.
       | false := filter l p
       }.
 
+  Equations filter_ {A} (l : list A) (p : A -> bool) : list A :=
+    filter nil p := nil; 
+    filter (cons a l) p with p a => { 
+      | true :=
+          a :: filter l p ;
+      | false
+        :=
+          filter l p
+      }.
+
   Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
     filter' (cons a l) p with p a =>
       { 
@@ -49,6 +66,16 @@ Module Equations.
       };
     filter' nil p := nil.
 
+  Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
+    filter' (cons a l) p with p a =>
+      { 
+      | true :=
+          a :: filter' l p ;
+      | false
+        := filter' l p
+      };
+    filter' nil p := nil.
+
   Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
     filter' (cons a l) p with p a =>
       { 
@@ -57,6 +84,16 @@ Module Equations.
       };
     filter' nil p := nil.
 
+  Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
+    filter' (cons a l) p with p a =>
+      { 
+        true :=
+          a :: filter' l p ;
+        false
+        := filter' l p
+      };
+    filter' nil p := nil.
+
   Equations filter'' {A} (l : list A) (p : A -> bool) : list A :=
     filter'' (cons a l) p with p a =>
       { | true := a :: filter'' l p ;

diff --git a/ci/test-indent/indent-inside-command-boxed.v b/ci/test-indent/indent-inside-command-boxed.v
@@ -1,9 +1,9 @@
 
 Require Export
-        Coq.Lists.List.
+  Coq.Lists.List.
 Require
   Export
-  Arith.
+    Arith.
 
 Module
   Mod.
@@ -38,7 +38,12 @@ Module
   Let x := 1.  Let y := 2.
 
   Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
-
+  Definition foo :=
+    foo x (y
+             a b)
+      z t  (* align with function foo + 2. *)
+      u v.  (* align with arg z on bol of previous line *)
+
 
   Inductive test
     : nat 
@@ -67,7 +72,7 @@ Module
 
   Lemma L4 : forall x:nat,
                Nat.iter x (A:=nat)
-                        (plus 2) 0 >= x.
+                 (plus 2) 0 >= x.
   Proof.
     idtac.
   Qed.
@@ -83,9 +88,9 @@ Module
   Qed.
 
   Lemma L1 : forall x:nat, Nat.iter x 
-                                    (A:=nat)
-                                    (plus 2)
-                                    0 >= x.
+                             (A:=nat)
+                             (plus 2)
+                             0 >= x.
   Proof.
     idtac.
   Qed.

diff --git a/ci/test-indent/indent-inside-command.v b/ci/test-indent/indent-inside-command.v
@@ -1,9 +1,9 @@
 
 Require Export
-        Coq.Lists.List.
+  Coq.Lists.List.
 Require
   Export
-  Arith.
+    Arith.
 
 Module
   Mod.
@@ -35,6 +35,18 @@ Module
     :=
     1.
 
+  Definition arith1 a
+    (b:nat) c
+    d e
+    :=
+    1.
+  Definition
+    arith1
+      (b:nat) c
+      d e
+    :=
+    1.
+
   Let x := 1.  Let y := 2.
 
   Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
@@ -56,7 +68,7 @@ Module
 
   Lemma L4 : forall x:nat,
       Nat.iter x (A:=nat)
-               (plus 2) 0 >= x.
+        (plus 2) 0 >= x.
   Proof.
     idtac.
   Qed.
@@ -72,9 +84,9 @@ Module
   Qed.
 
   Lemma L1 : forall x:nat, Nat.iter x 
-                                    (A:=nat)
-                                    (plus 2)
-                                    0 >= x.
+                             (A:=nat)
+                             (plus 2)
+                             0 >= x.
   Proof.
     idtac.
   Qed.

diff --git a/ci/test-indent/indent-tac.v b/ci/test-indent/indent-tac.v
@@ -280,16 +280,16 @@ Module GoalSelectors.
     [aa]:{ auto. }
     2:{  auto. }
     [ee]:auto.
-    {  auto.}
+    {  auto. }
   Qed.
   (* Same without space between "." and "}". *)
   Theorem lt_n_S2 : (True \/ True \/ True \/ True \/ True ) -> True.
   Proof.
     refine (or_ind ?[aa] (or_ind ?[bb] (or_ind ?[cc] (or_ind ?[dd] ?[ee])))).
-    [aa]:{ auto.}
-    2:{  auto.}
+    [aa]:{ auto. }
+    2:{  auto. }
     [ee]:auto.
-    {  auto.}
+    {  auto. }
   Qed.
 
 
@@ -404,6 +404,21 @@ Module X.
       {auto. }
       {auto. }
     }
+    intros r. {
+      exists
+        {|
+          fld1:=
+            r.(fld2);
+          fld2
+          :=r.(fld1);
+          fld3
+          :=
+            false
+        |}.
+      split.
+      {auto. }
+      {auto. }
+    }
     auto.
     auto.
   Qed.

diff --git a/coq/coq-mode.el b/coq/coq-mode.el
@@ -214,6 +214,7 @@ Near here means PT is either inside or just aside of a comment."
   (smie-setup coq-smie-grammar #'coq-smie-rules
               :forward-token #'coq-smie-forward-token
               :backward-token #'coq-smie-backward-token)
+  (add-hook 'smie-indent-functions #'coq-smie--args nil t)
 
   ;; old indentation code.
   ;; (require 'coq-indent)