X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=87944aa34f23a98028573c59c3a445fef78ae1c5;hb=cbe0302d6b0d2bca6657fa7479a62d0004665612;hp=65e1c32c7e16ec85a676c4a18e900c03ae54c79f;hpb=29969baf115afff7eb9ea9e2ca98d40ab7006dcc;p=helm.git

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 65e1c32c7..87944aa34 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -93,6 +93,8 @@ and countterm current_size t =
     | A.Num (s, _) -> current_size + String.length s
     | A.Sort _ -> current_size + 4 (* sort name *)
     | A.Symbol (s,_) -> current_size + String.length s
+
+    | A.UserInput -> current_size
 ;;
 
 let is_big t = 
@@ -282,17 +284,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) ->
@@ -317,6 +330,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
     | A.Symbol (s, _) -> 
         Box.Text([],s)
 
+    | A.UserInput -> Box.Text([],"")
+
   and aux_option ~tail = function
       None  -> Box.Text([],"_")
     | Some ast -> ast2box ~tail ast 
@@ -366,11 +381,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 =
@@ -452,6 +467,7 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
     | A.Sort `Type -> P.Mtext ([], "Type")
     | A.Sort `CProp -> P.Mtext ([], "CProp")
     | A.Implicit -> P.Mtext([], "?")
+    | A.UserInput -> P.Mtext([], "")
     | A.Appl [] -> assert false
     | A.Appl ((hd::tl) as l) ->
         let rec find_symbol idref = function