[pp] Force well-formed boxes by construction.

We replace open/close box commands in favor of the create box ones.

3 files changed, 8 insertions, 27 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 4ff10b4d7..388eed9e4 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -32,13 +32,12 @@ type std_ppcmds =
   | Ppcmd_string of string
   | Ppcmd_glue of std_ppcmds list
   | Ppcmd_box  of block_type * std_ppcmds
+  | Ppcmd_tag of pp_tag * std_ppcmds
+  (* Are those redundant? *)
   | Ppcmd_print_break of int * int
   | Ppcmd_white_space of int
   | Ppcmd_force_newline
-  | Ppcmd_open_box of block_type
-  | Ppcmd_close_box
   | Ppcmd_comment of string list
-  | Ppcmd_tag of pp_tag * std_ppcmds
 
 (* Compute length of an UTF-8 encoded string
    Rem 1 : utf8_length <= String.length (equal if pure ascii)
@@ -137,13 +136,6 @@ let v   n s = Ppcmd_box(Pp_vbox n,s)
 let hv  n s = Ppcmd_box(Pp_hvbox n,s)
 let hov n s = Ppcmd_box(Pp_hovbox n,s)
 
-(* Opening and closing of boxes *)
-let hb   n   = Ppcmd_open_box(Pp_hbox n)
-let vb   n   = Ppcmd_open_box(Pp_vbox n)
-let hvb  n   = Ppcmd_open_box(Pp_hvbox n)
-let hovb n   = Ppcmd_open_box(Pp_hovbox n)
-let close () = Ppcmd_close_box
-
 (* Opening and closed of tags *)
 let tag t s = Ppcmd_tag(t,s)
 
@@ -191,8 +183,6 @@ let pp_with ?pp_tag ft =
         cpp_open_box bty ;
         if not (Format.over_max_boxes ()) then pp_cmd ss;
         Format.pp_close_box ft ()
-    | Ppcmd_open_box bty      -> cpp_open_box bty
-    | Ppcmd_close_box         -> pp_close_box ft ()
     | Ppcmd_white_space n     -> pp_print_break ft n 0
     | Ppcmd_print_break(m,n)  -> pp_print_break ft m n
     | Ppcmd_force_newline     -> pp_force_newline ft ()
diff --git a/lib/pp.mli b/lib/pp.mli
index ed97226ae..cee7fa052 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -22,13 +22,12 @@ type std_ppcmds =
   | Ppcmd_string of string
   | Ppcmd_glue of std_ppcmds list
   | Ppcmd_box  of block_type * std_ppcmds
+  | Ppcmd_tag  of pp_tag * std_ppcmds
+  (* Are those redundant? *)
   | Ppcmd_print_break of int * int
   | Ppcmd_white_space of int
   | Ppcmd_force_newline
-  | Ppcmd_open_box of block_type
-  | Ppcmd_close_box
   | Ppcmd_comment of string list
-  | Ppcmd_tag of pp_tag * std_ppcmds
 
 (** {6 Formatting commands} *)
 
@@ -69,15 +68,7 @@ val v : int -> std_ppcmds -> std_ppcmds
 val hv : int -> std_ppcmds -> std_ppcmds
 val hov : int -> std_ppcmds -> std_ppcmds
 
-(** {6 Opening and closing of boxes} *)
-
-val hb : int -> std_ppcmds
-val vb : int -> std_ppcmds
-val hvb : int -> std_ppcmds
-val hovb : int -> std_ppcmds
-val close : unit -> std_ppcmds
-
-(** {6 Opening and closing of tags} *)
+(** {6 Tagging} *)
 
 val tag : pp_tag -> std_ppcmds -> std_ppcmds
 
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 8b9261113..1ad4d622b 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -505,12 +505,12 @@ let pp_mapint map =
 		pp_form obj ++ str " => " ++
 				 pp_list (fun (i,f) -> pp_form f) l ++
 				 cut ()) ) map;
-    str "{ " ++ vb 0 ++  (!pp) ++ str " }" ++ close ()
+    str "{ " ++ hv 0 (!pp ++ str " }")
 
 let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
 
 let pp_gl gl= cut () ++
-  str "{ " ++ vb 0 ++
+  str "{ " ++ hv 0 (
 	      begin
 		match gl.abs with
 		    None -> str ""
@@ -520,7 +520,7 @@ let pp_gl gl= cut () ++
   str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
   str "arrows=" ++ pp_mapint gl.right ++ cut () ++
   str "cnx   =" ++ pp_list pp_connect gl.cnx ++ cut () ++
-  str "goal  =" ++ pp_form gl.gl ++ str " }" ++ close ()
+  str "goal  =" ++ pp_form gl.gl ++ str " }")
 
 let pp =
   function