Merge PR#722: [printing] Remove duplicated printing function.

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
+