From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 20 Jan 2007 15:31:18 +0000 (+0000)
Subject: Bug fixed: if the context of a sequent was empty a vertical box without content
X-Git-Tag: 0.4.95@7852~654
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d75d51c031efee5e30d9db9c11f88939e8614ad9;p=helm.git

Bug fixed: if the context of a sequent was empty a vertical box without content
was generated. This is not allowed by BoxPp (assert failure).
---

diff --git a/components/content_pres/sequent2pres.ml b/components/content_pres/sequent2pres.ml
index 88c804b7d..391b178a2 100644
--- a/components/content_pres/sequent2pres.ml
+++ b/components/content_pres/sequent2pres.ml
@@ -83,16 +83,17 @@ let sequent2pres term2pres (_,_,context,ty) =
          aux (r::accum) tl
       | _::_ -> assert false in
       aux [] context in
- let pres_context = (Box.b_v [] (context2pres context)) in
+ let pres_context =
+  if context <> [] then [Box.b_v [] (context2pres context)] else [] in
  let pres_goal = term2pres ty in 
  (Box.b_h [] [
    Box.b_space; 
    (Box.b_v []
-      [Box.b_space;
-       pres_context;
+      (Box.b_space ::
+       pres_context @ [
        b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
        Box.b_space; 
-       pres_goal])])
+       pres_goal]))])
 
 let sequent2pres ~ids_to_inner_sorts =
   sequent2pres