* added popup menu, implemented some functions

[helm.git] / helm / ocaml / cic_transformations / cexpr2pres.ml

diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml
index 841ccf3da57e3f58d4c69070b889ef89b2e22b2f..f6a3b490d48e4f1e3a717a27ebb015c28e02be31 100644 (file)
--- a/helm/ocaml/cic_transformations/cexpr2pres.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres.ml
@@ -49,7 +49,13 @@ let countterm current_size t =
         let c1 = current_size + (String.length name) in 
         countsubst subst c1
     | CE.LocalVar (_,name) -> current_size + (String.length name)
-    | CE.Meta (_,name) -> current_size + (String.length name)
+    | CE.Meta (_,name,l) ->
+       List.fold_left
+        (fun i t ->
+          match t with
+             None -> i
+           | Some t' -> aux i t'
+        ) (current_size + String.length name) l
     | CE.Num (_,value) -> current_size + (String.length value)
     | CE.Appl (_,l) -> 
         List.fold_left aux current_size l
@@ -89,7 +95,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 +108,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 +136,32 @@ 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
-        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.Meta (xref,name,l) ->
+        let attr = make_attributes [Some "helm","xref"] [xref] in
+        let l' =
+         List.map
+          (function
+              None -> P.Mo [] "_"
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ 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 +169,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 +185,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 +199,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 +214,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 +250,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 +276,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 +304,32 @@ 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
-        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.Meta (xref,name,l) ->
+        let attr = make_attributes [Some "helm","xref"] [xref] in
+        let l' =
+         List.map
+          (function
+              None -> P.Mo [] "_"
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ 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 +342,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 +352,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 +366,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 +374,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 +389,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 +404,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 
                [] -> []