Misc indentatiosn requests

[cpitclaudel]

Hi folks,

How hard would it be to fix the following indentation issue?

let x := (eval compute in y) in
exact x. (* indents correctly *)

let x := eval compute in y in
    exact x. (* indents incorrectly *)

Besides that, could we make indentation of continuation lines in functions configurable?

(* current style: *)
List.fold_right (fun x acc =>
                   f x (g acc))
                ast fields.

(* ocaml style *)
List.fold_right (fun x acc ->
    f x (g acc))
  ast fields.

(* current style *)
match goal with
| 0 => fun v => nil
| S n => fun v =>
          f (vhd v) (vtl v)
end

(* convoy pattern style *)
match goal with
| 0 => fun v => nil
| S n => fun v =>
  f (vhd v) (vtl v)
end

Thanks!

[monnier]

Besides that, could we make indentation of continuation lines in functions configurable?

(* current style: *)
List.fold_right (fun x acc =>
                   f x (g acc))
                ast fields.

(* ocaml style *)
List.fold_right (fun x acc ->
    f x (g acc))
  ast fields.

I think this one is not just about "indentation of continuation lines in functions configurable" but also about indentation of arguments. I.e. about the difference between

List.fold_right myfunc
  ast fields

and

List.fold_right myfunc
                ast fields

( current style ) match goal with | 0 => fun v => nil | S n => fun v => f (vhd v) (vtl v) end

( convoy pattern style ) match goal with | 0 => fun v => nil | S n => fun v => f (vhd v) (vtl v) end

This one at least should be fairly easy. Something like:

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 6a92113d..03e74501 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1231,6 +1231,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
                    ))))
           `(column . ,(if (smie-rule-hanging-p) pcol (+ 2 pcol)))))

+       ((equal token "fun")
+        (when (smie-rule-prev-p "=>") (smie-rule-parent)))
+
        ((equal token "|")
    (cond ((smie-rule-parent-p "with match")
           (- (funcall smie-rules-function :after "with match") 2))

might do the trick (untested, tho: probably won't work as is).

    Stefan