Commit db5b23ea authored by POTTIER Francois's avatar POTTIER Francois

Pretty-printing improvements.

parent 4a06dd7f
......@@ -184,7 +184,7 @@ and expr e =
(* -------------------------------------------------------------------------- *)
(* Typed variables: [x : T]. *)
(* Typed variables: [x : t]. *)
(* Raw. *)
......@@ -194,7 +194,7 @@ let var (x, t) =
(* With parentheses and with a leading space. *)
let pvar xt =
break 1 ^^ parens (var xt)
space ^^ parens (var xt)
let pvars xts =
concat_map pvar xts
......@@ -211,13 +211,11 @@ let fields xts =
(* A definition, without a leading keyword, but with a leading space.
[ x : d1 := d2]. *)
let definition x d1 d2 =
let definition x d1 =
block
(space ^^ x ^^ colon)
(break 1 ^^ d1)
(break 1 ^^ string ":=")
^/^
d2
(* A parameter, without a leading keyword, but with a leading space.
[ x : d1]. *)
......@@ -238,7 +236,7 @@ let record_rhs r =
let sum_rhs r =
concat_map (fun xt ->
hardline ^^ string "| " ^^ var xt
hardline ^^ block (string "| ") (var xt) empty
) r.coqind_branches
(* The left-hand side of a record or sum declaration. [ foo params : T := rhs]. *)
......@@ -247,7 +245,8 @@ let inductive_lhs rhs r =
definition
(string r.coqind_name ^^ pvars r.coqind_targs)
(expr r.coqind_ret)
(rhs r)
^^
rhs r
(* An implicit argument specification. *)
......@@ -265,10 +264,8 @@ let implicit (x, i) =
let top = function
| Coqtop_def ((x, e1), e2) ->
string "Definition" ^^
definition
(string x) (expr e1)
(expr e2)
^^ dot
definition (string x) (expr e1) ^/^
expr e2 ^^ dot
| Coqtop_param (x, e1) ->
string "Parameter" ^^
parameter x (expr e1)
......@@ -298,7 +295,7 @@ let top = function
sprintf "Notation \"''%s'\" := (%s) (at level 0) : atom_scope." x (value_variable n)
| Coqtop_implicit (x, xs) ->
string "Implicit Arguments " ^^
string x ^^
string x ^/^
brackets (separate_map space implicit xs)
^^ dot
| Coqtop_register (db, x, v) ->
......
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