diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/miscprint.ml | 25 | ||||
| -rw-r--r-- | printing/miscprint.mli | 13 |
2 files changed, 38 insertions, 0 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 360843711c..a4ecbdf5e5 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -47,3 +47,28 @@ let pr_move_location pr_id = function | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id | MoveFirst -> str " at top" | MoveLast -> str " at bottom" + +(** Printing of bindings *) +let pr_binding prc = function + | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + +let pr_bindings prc prlc = function + | ImplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + pr_sequence prc l + | ExplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | NoBindings -> mt () + +let pr_bindings_no_with prc prlc = function + | ImplicitBindings l -> + brk (0,1) ++ prlist_with_sep spc prc l + | ExplicitBindings l -> + brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | NoBindings -> mt () + +let pr_with_bindings prc prlc (c,bl) = + hov 1 (prc c ++ pr_bindings prc prlc bl) + diff --git a/printing/miscprint.mli b/printing/miscprint.mli index fe8c779ff4..dbbe3dcfd8 100644 --- a/printing/miscprint.mli +++ b/printing/miscprint.mli @@ -22,3 +22,16 @@ val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds val pr_move_location : ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds + +val pr_bindings : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + +val pr_bindings_no_with : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + +val pr_with_bindings : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds + |