X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=35f128a05b524078b117a394cb51b87a8554f6d1;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=abd7ab0410b628de77835376ea2186c2136a73e1;hpb=29dce796091e98b5bfe48423189453eaad449bda;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index abd7ab041..35f128a05 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
@@ -331,7 +332,7 @@ let render ids_to_uris ?(prec=(-1)) =
           | `Raw _ -> ()
           | `Level (-1) -> reset := true
           | `Level child_prec ->
-              assert (!expected_level = None);
+(*               assert (!expected_level = None); *)
               expected_level := !inferred_level;
               inferred_level := Some child_prec
           | `IdRef xref -> new_xref := xref :: !new_xref
@@ -344,7 +345,7 @@ let render ids_to_uris ?(prec=(-1)) =
             | Some prec -> prec
           in
           (match !inferred_level with
-          | None -> aux !new_xmlattrs mathonly new_xref prec t 
+          | None -> aux !new_xmlattrs mathonly new_xref prec t
           | Some child_prec ->
               let t' = aux !new_xmlattrs mathonly new_xref child_prec t in
               (*prerr_endline 
@@ -399,6 +400,20 @@ let render ids_to_uris ?(prec=(-1)) =
             (CicNotationUtil.ungroup terms)
         in
         box_of mathonly kind attrs children
+    | A.Mstyle (l,terms) -> 
+        Mpres.Mstyle 
+          (List.map (fun (k,v) -> None,k,v) l, 
+           box_of mathonly (A.H, false, false) attrs 
+            (aux_children mathonly false xref  prec 
+              (CicNotationUtil.ungroup terms)))
+    | A.Mpadded (l,terms) -> 
+        Mpres.Mpadded 
+          (List.map (fun (k,v) -> None,k,v) l, 
+           box_of mathonly (A.H, false, false) attrs 
+            (aux_children mathonly false xref  prec 
+              (CicNotationUtil.ungroup terms)))
+    | A.Maction alternatives -> 
+         toggle_action (List.map invoke_reinit alternatives)
     | A.Group terms ->
 	let children =
           aux_children mathonly false xref  prec