X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=82a326c48bbb4ffc70d64400ef043b1b74955fa0;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=1a092909e113cdafcd00343281d5b9192c2056b8;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 1a092909e..82a326c48 100644
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -200,16 +200,17 @@ let add_parens child_prec curr_prec t =
       BoxPp.render_to_string (function x::_->x|_->assert false)
         ~map_unicode_to_tex:false 80 t);*)t)
 
-let render ids_to_uris ?(prec=(-1)) =
+let lookup_uri ids_to_uris id =
+ try
+   let uri = Hashtbl.find ids_to_uris id in
+   Some (UriManager.string_of_uri uri)
+ with Not_found -> None
+;;
+
+let render ~lookup_uri ?(prec=(-1)) =
   let module A = Ast in
   let module P = Mpresentation in
 (*   let use_unicode = true in *)
-  let lookup_uri id =
-    (try
-      let uri = Hashtbl.find ids_to_uris id in
-      Some (UriManager.string_of_uri uri)
-    with Not_found -> None)
-  in
   let make_href xmlattrs xref =
     let xref_uris =
       List.fold_right
@@ -370,6 +371,9 @@ let render ids_to_uris ?(prec=(-1)) =
       (* use the one below to reset precedence and associativity *)
     let invoke_reinit t = aux [] mathonly xref ~-1 t in
     match l with
+    | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
+    | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
+      -> Mpres.Msubsup (attrs, invoke' t1, invoke_reinit t2, invoke_reinit t3)
     | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2)
     | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2)
     | A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke_reinit t2)