snapshot

[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index d815506378f90924fa8cd79eda5f4b2cbf09e5bb..a3e4f46211a97a2b5fef1399fd6c50a063e3f9ed 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -118,6 +118,13 @@ and pp_capture_variable = function
   | term, None -> pp_term term
   | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")"
 
+and pp_box_spec (kind, spacing, indent) =
+  let int_of_bool b = if b then 1 else 0 in
+  let kind_string =
+    match kind with H -> "H" | V -> "V" | HV -> "HV" | HOV -> "HOV"
+  in
+  sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent)
+
 and pp_layout = function
   | Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
   | Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
@@ -130,14 +137,10 @@ and pp_layout = function
   | Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
 (*   | Break -> "\\BREAK" *)
-  | Box (H, terms) ->
-      sprintf "\\HBOX [%s]" (String.concat " " (List.map pp_term terms))
-  | Box (V, terms) ->
-      sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms))
-  | Box (HV, terms) ->
-      sprintf "\\HVBOX [%s]" (String.concat " " (List.map pp_term terms))
-  | Box (HOV, terms) ->
-      sprintf "\\HOVBOX [%s]" (String.concat " " (List.map pp_term terms))
+(*   | Space -> "\\SPACE" *)
+  | Box (box_spec, terms) ->
+      sprintf "\\%s [%s]" (pp_box_spec box_spec)
+        (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
   | List0 (t, sep_opt) ->