From 5eb0f57378da1394b08d593dc723301191873565 Mon Sep 17 00:00:00 2001
From: Luca Padovani <luca.padovani@unito.it>
Date: Tue, 2 Nov 2004 14:29:11 +0000
Subject: [PATCH] * substitution are not rendered by default, an action is
 generated

---
 helm/ocaml/cic_transformations/ast2pres.ml | 33 ++++++++++++++--------
 1 file changed, 22 insertions(+), 11 deletions(-)

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 65e1c32c7..cafd80c4a 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -282,17 +282,28 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
             function
               [] -> []
             | [(s,t)] -> 
-                make_subst start_txt s t "]"
+                make_subst start_txt s t ""
             | (s,t)::tl ->
-                (make_subst start_txt s t ";")@(make_substs " " tl)
+                (make_subst start_txt s t ";")@(make_substs "" tl)
           in
           match subst with
-          | Some subst -> make_substs ((map_tex unicode "subst") ^ "[") subst
-          | None -> []
+          | Some subst ->
+	      Box.H([],
+	            [Box.Text(make_std_attributes xref,s);
+		     Box.Action([],
+		       [Box.Text([],"[...]");
+		        Box.H([], [Box.Text([], map_tex unicode "subst" ^ "[");
+	                 Box.V([], make_substs "" subst);
+		         Box.Text([], "]")])])])
+          | None -> Box.Text(make_std_attributes xref, s)
         in
-        Box.V([], (* attr here or on Vbox? *)
+	 subst
+	(*
+        Box.H([], (* attr here or on Vbox? *)
               [Box.Text(make_std_attributes xref,s);
-               Box.indent(Box.V([],subst))])
+	       Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])])
+               (* Box.indent(Box.V([],subst))]) *)
+	*)
     | A.Implicit -> 
         Box.Text([],"_") (* big? *)
     | A.Meta (n, l) ->
@@ -366,11 +377,11 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
 
   and make_subst start_txt varname body end_txt =
     pretty_append ~tail:[end_txt]
-      [Box.Text([],start_txt);
-       Box.Text([],varname);
-       Box.smallskip;
-       Box.Text([],map_tex unicode "Assign")
-      ]
+      ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@
+       [Box.Text([],varname);
+        Box.smallskip;
+        Box.Text([],map_tex unicode "Assign")
+       ])
       body
             
   and pretty_append ~tail l ast =
-- 
2.39.2