X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;h=40f185dcdbc773ed5d2b03b08d8a97ea6074e05a;hb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;hp=841ccf3da57e3f58d4c69070b889ef89b2e22b2f;hpb=b266dce15b2f669a70daaee3bd0887f8d9c345b2;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml
index 841ccf3da..40f185dcd 100644
--- a/helm/ocaml/cic_transformations/cexpr2pres.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres.ml
@@ -89,7 +89,9 @@ let rec make_attributes l1 =
   function
       [] -> []
     | None::tl -> make_attributes (List.tl l1) tl
-    | (Some s)::tl -> (List.hd l1,s)::(make_attributes (List.tl l1) tl)
+    | (Some s)::tl ->
+       let p,n = List.hd l1 in
+        (p,n,s)::(make_attributes (List.tl l1) tl)
 ;;
 
 let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
@@ -100,14 +102,14 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
       CE.Symbol (xref,name,None,uri) -> 
         let attr = 
          make_attributes 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow([],P.Mi (attr,name)::tail)
     | CE.Symbol (xref,name,Some subst,uri) ->
         let attr = 
          make_attributes 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
         let rec make_subst =
           (function 
                [] -> assert false
@@ -128,23 +130,23 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
           (make_subst subst)@
           (P.Mtext([],"]")::tail))
     | CE.LocalVar (xref,name) -> 
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow([],P.Mi (attr,name)::tail)
     | CE.Meta (xref,name) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow([],P.Mi (attr,name)::tail)
     | CE.Num (xref,value) -> 
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
           P.Mn (attr,value)
         else P.Mrow([],P.Mn (attr,value)::tail)
     | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
-        let aattr = make_attributes ["helm:xref"] [axref] in
-        let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
+        let aattr = make_attributes [Some "helm","xref"] [axref] in
+        let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
         (try 
           (let f = Hashtbl.find symbol_table n in
            f tl ~priority ~assoc ~tail aattr sattr)
@@ -152,11 +154,11 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
            P.Mrow(aattr,
            P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
     | CE.Appl (xref,l) as t ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some"helm","xref"] [xref] in
         P.Mrow(attr,
            P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
     | CE.Binder (xref, kind,(n,s),body) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let binder = 
           if kind = "Lambda" then 
              Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
@@ -168,13 +170,13 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
              Netconversion.ustring_of_uchar `Enc_utf8 0x2203
           else "unknown" in
         P.Mrow (attr, 
-           P.Mtext([("mathcolor","Blue")],binder)::
+           P.Mtext([None,"mathcolor","Blue"],binder)::
            P.Mtext([],n ^ ":")::
            (aux s)::
            P.Mo([],".")::
            (aux body)::tail)
     | CE.Letin (xref,(n,s),body) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         P.Mrow (attr, 
            P.Mtext([],("let "))::
            P.Mtext([],(n ^ "="))::
@@ -182,7 +184,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
            P.Mtext([]," in ")::
            (aux body)::tail)
     | CE.Letrec (xref,defs,body) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let rec make_defs =
           (function 
                [] -> assert false
@@ -197,7 +199,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
            (P.Mtext([]," in ")::
            (aux body)::tail))
     | CE.Case (xref,a,np) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let rec make_patterns =
           (function 
                [] -> []
@@ -233,7 +235,7 @@ let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
       if c > maxsize then
         P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
         (make_args_charcount ~tail:tail tl)
-      else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([("width","0.2cm")]))::(make_args ~tail:tail l)))])]
+      else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
 
 (* 
   function 
@@ -259,14 +261,14 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
       CE.Symbol (xref,name,None,uri) -> 
         let attr = 
          make_attributes 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow ([],P.Mi (attr,name)::tail)
     | CE.Symbol (xref,name,Some subst,uri) ->
         let attr = 
          make_attributes 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
         let rec make_subst =
           (function 
                [] -> assert false
@@ -287,23 +289,23 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
           (make_subst subst)@
           (P.Mtext([],"]")::tail))
     | CE.LocalVar (xref,name) -> 
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow ([],P.Mi (attr,name)::tail)
     | CE.Meta (xref,name) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
           P.Mi (attr,name)
         else P.Mrow ([],P.Mi (attr,name)::tail)
     | CE.Num (xref,value) -> 
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         if tail = [] then
           P.Mn (attr,value)
         else P.Mrow ([],P.Mn (attr,value)::tail)
     | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
-        let aattr = make_attributes ["helm:xref"] [axref] in
-        let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
+        let aattr = make_attributes [Some "helm","xref"] [axref] in
+        let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
         if (is_big t) then
           (try 
             (let f = Hashtbl.find symbol_table_charcount n in
@@ -316,7 +318,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
               make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
         else cexpr2pres t
     | CE.Appl (xref,l) as t ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         if (is_big t) then
           P.Mtable (attr@P.standard_tbl_attr,
             P.Mtr([],[P.Mtd([],P.Mrow([],
@@ -326,7 +328,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
         else cexpr2pres t
     | CE.Binder (xref, kind,(n,s),body) as t ->
         if (is_big t) then
-          let attr = make_attributes ["helm:xref"] [xref] in
+          let attr = make_attributes [Some "helm","xref"] [xref] in
           let binder = 
             if kind = "Lambda" then 
               Netconversion.ustring_of_uchar `Enc_utf8 0x03bb  
@@ -340,7 +342,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
           P.Mtable (attr@P.standard_tbl_attr,
              [P.Mtr ([],[P.Mtd ([],
                P.Mrow([],
-                [P.Mtext([("mathcolor","Blue")],binder);
+                [P.Mtext([None,"mathcolor","Blue"],binder);
                  P.Mtext([],n ^ ":");
                  cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
               P.Mtr ([],[P.Mtd ([],
@@ -348,11 +350,11 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
         else (cexpr2pres t ~tail:tail)
     | CE.Letin (xref,(n,s),body) as t ->
         if (is_big t) then
-          let attr = make_attributes ["helm:xref"] [xref] in
+          let attr = make_attributes [Some "helm","xref"] [xref] in
           P.Mtable (attr@P.standard_tbl_attr,
              [P.Mtr ([],[P.Mtd ([],
                P.Mrow([],
-                [P.Mtext([("mathcolor","Blue")],"let");
+                [P.Mtext([None,"mathcolor","Blue"],"let");
                  P.smallskip;
                  P.Mtext([],n ^ "=");
                  cexpr2pres_charcount s;
@@ -363,7 +365,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
                P.indented (cexpr2pres_charcount body))])])
         else (cexpr2pres t)
     | CE.Letrec (xref,defs,body) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let rec make_defs =
           (function 
                [] -> assert false
@@ -378,7 +380,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
           [P.Mtext([]," in ");
            (aux body)])
     | CE.Case (xref,a,np) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let rec make_patterns =
           (function 
                [] -> []