Commit 56bb1e16 authored by POTTIER Francois's avatar POTTIER Francois

Various pretty-printing improvements.

parent db5b23ea
......@@ -83,6 +83,22 @@ let parens d =
(break 0 ^^ d)
(break 0 ^^ rparen)
(* Braces with spacing and indentation. *)
let braces d =
block
lbrace
(break 1 ^^ d)
(break 1 ^^ rbrace)
(* Brackets with spacing and indentation. *)
let brackets d =
block
lbracket
(break 1 ^^ d)
(break 1 ^^ rbracket)
(* -------------------------------------------------------------------------- *)
(* Tuples. *)
......@@ -189,7 +205,7 @@ and expr e =
(* Raw. *)
let var (x, t) =
string x ^^ colon ^/^ expr t
block (string x ^^ colon) (space ^^ expr t) empty
(* With parentheses and with a leading space. *)
......@@ -209,7 +225,7 @@ let fields xts =
(* Toplevel elements. *)
(* A definition, without a leading keyword, but with a leading space.
[ x : d1 := d2]. *)
[ x : d1 :=]. *)
let definition x d1 =
block
......@@ -218,17 +234,18 @@ let definition x d1 =
(break 1 ^^ string ":=")
(* A parameter, without a leading keyword, but with a leading space.
[ x : d1]. *)
[ x : d1.]. *)
let parameter x d1 =
block
(space ^^ string x ^^ colon)
(space ^^ x ^^ colon)
(break 1 ^^ d1)
empty
dot
(* The right-hand side of a record declaration. [Foo { ... }]. *)
let record_rhs r =
space ^^
string (r.coqind_name ^ "_of") ^^ space ^^
braces (fields r.coqind_branches)
......@@ -268,16 +285,13 @@ let top = function
expr e2 ^^ dot
| Coqtop_param (x, e1) ->
string "Parameter" ^^
parameter x (expr e1)
^^ dot
parameter (string x) (expr e1)
| Coqtop_instance ((x, e1), global) ->
string ((if global then "Global " else "") ^ "Instance") ^^
parameter x (expr e1)
^^ dot
parameter (string x) (expr e1)
| Coqtop_lemma (x, e1) ->
string "Lemma" ^^
parameter x (expr e1)
^^ dot
parameter (string x) (expr e1)
| Coqtop_proof s ->
sprintf "Proof. %s Qed." s
| Coqtop_record r ->
......
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