Commit 9ded32ff authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Redefine [parens] using [block]. Extract global parameters.

parent 916af86d
...@@ -3,6 +3,16 @@ open Coq ...@@ -3,6 +3,16 @@ open Coq
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* Global parameters. *)
let indentation =
2
let width =
80
(* -------------------------------------------------------------------------- *)
(* Various fixed elements. *) (* Various fixed elements. *)
let arrow = let arrow =
...@@ -30,7 +40,7 @@ let quote = ...@@ -30,7 +40,7 @@ let quote =
let app d1 d2 = let app d1 d2 =
(* The following definition would reject a large argument on a line of (* The following definition would reject a large argument on a line of
its own, indented: *) its own, indented: *)
(* group (d1 ^^ nest 2 (break 1 ^^ d2)) *) (* group (d1 ^^ nest indentation (break 1 ^^ d2)) *)
(* However, that would be redundant with the fact that large arguments (* However, that would be redundant with the fact that large arguments
are usually parenthesized, and we already break lines and indent are usually parenthesized, and we already break lines and indent
within the parentheses. So, the following suffices: *) within the parentheses. So, the following suffices: *)
...@@ -50,6 +60,9 @@ let apps ds = ...@@ -50,6 +60,9 @@ let apps ds =
let block n opening contents closing = let block n opening contents closing =
group (opening ^^ nest n (contents) ^^ closing) group (opening ^^ nest n (contents) ^^ closing)
let block =
block indentation
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* Parentheses with indentation. *) (* Parentheses with indentation. *)
...@@ -58,10 +71,10 @@ let block n opening contents closing = ...@@ -58,10 +71,10 @@ let block n opening contents closing =
opening and closing parentheses alone on a line and indenting the content. *) opening and closing parentheses alone on a line and indenting the content. *)
let parens d = let parens d =
group ( block
nest 2 (lparen ^^ break 0 ^^ d) ^^ lparen
break 0 ^^ rparen (break 0 ^^ d)
) (break 0 ^^ rparen)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
...@@ -136,21 +149,21 @@ and expr2 = function ...@@ -136,21 +149,21 @@ and expr2 = function
and expr3 = function and expr3 = function
| Coq_lettuple (es, e1, e2) -> | Coq_lettuple (es, e1, e2) ->
block 2 block
(string "let '" ^^ tuple expr es ^^ colonequals) (string "let '" ^^ tuple expr es ^^ colonequals)
(break 1 ^^ expr e1) (break 1 ^^ expr e1)
(break 1 ^^ within) (break 1 ^^ within)
^/^ ^/^
expr3 e2 expr3 e2
| Coq_forall ((x, e1), e2) -> | Coq_forall ((x, e1), e2) ->
block 2 block
(string "forall " ^^ string x ^^ colon) (string "forall " ^^ string x ^^ colon)
(break 1 ^^ expr e1 ^^ comma) (break 1 ^^ expr e1 ^^ comma)
empty empty
^/^ ^/^
expr3 e2 expr3 e2
| Coq_fun ((x, e1), e2) -> | Coq_fun ((x, e1), e2) ->
block 2 block
(string "fun" ^^ space ^^ string x ^^ colon) (string "fun" ^^ space ^^ string x ^^ colon)
(break 1 ^^ expr e1) (break 1 ^^ expr e1)
(break 1 ^^ doublearrow) (break 1 ^^ doublearrow)
...@@ -166,7 +179,6 @@ and expr e = ...@@ -166,7 +179,6 @@ and expr e =
let expr e : string = let expr e : string =
let b = Buffer.create 1024 in let b = Buffer.create 1024 in
PPrintEngine.ToBuffer.pretty 0.9 80 b (expr e); PPrintEngine.ToBuffer.pretty 0.9 width b (expr e);
Buffer.contents b Buffer.contents b
(* TEMPORARY allow choosing the width *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment