Xml.token is now namespace-aware. As a consequence, xml2Gdomexmath is

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

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 019538169e4669aecea0b26832a1463debaeec12..5d6923237e0b73ad25800f92edea881365d9f6bf 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -119,26 +119,26 @@ let make_row items concl =
   let module P = Mpresentation in
     (match concl with 
        P.Mtable _ -> (* big! *)
-         P.Mtable ([("align","baseline 1");("equalrows","false");
-          ("columnalign","left")],
+         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+          None,"columnalign","left"],
            [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]);
             P.Mtr ([],[P.Mtd ([],P.indented concl)])])
      | _ ->  (* small *)
-       P.Mrow([],items@[P.Mspace([("width","0.1cm")]);concl]))
+       P.Mrow([],items@[P.Mspace([None,"width","0.1cm"]);concl]))
 ;;
 
 let make_concl verb concl =
   let module P = Mpresentation in
     (match concl with 
        P.Mtable _ -> (* big! *)
-         P.Mtable ([("align","baseline 1");("equalrows","false");
-          ("columnalign","left")],
-           [P.Mtr([],[P.Mtd ([],P.Mtext([("mathcolor","Red")],verb))]);
+         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+          None,"columnalign","left"],
+           [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]);
             P.Mtr ([],[P.Mtd ([],P.indented concl)])])
      | _ ->  (* small *)
        P.Mrow([],
-        [P.Mtext([("mathcolor","Red")],verb); 
-         P.Mspace([("width","0.1cm")]);
+        [P.Mtext([None,"mathcolor","Red"],verb); 
+         P.Mspace([None,"width","0.1cm"]);
          concl]))
 ;;
 
@@ -157,10 +157,10 @@ let make_args_for_apply term2pres args =
     | Con.Term t -> 
         if is_first then
           (term2pres t)::row
-        else P.Mspace([("width","0.1cm")])::P.Mi([],"_")::row
+        else P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row
     | Con.ArgProof _ 
     | Con.ArgMethod _ -> 
-       P.Mspace([("width","0.1cm")])::P.Mi([],"_")::row) in
+       P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row) in
  match args with 
    hd::tl -> 
      make_arg_for_apply true hd 
@@ -177,7 +177,7 @@ let rec justification term2pres p =
     let pres_args = 
       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
     P.Mrow([],
-      P.Mtext([("mathcolor","Red")],"by")::P.Mspace([("width","0.1cm")])::
+      P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
       P.Mo([],"(")::pres_args@[P.Mo([],")")]) 
   else proof2pres term2pres p 
      
@@ -215,11 +215,11 @@ and proof2pres term2pres p =
                None -> P.Mtext([],"NO PROOF!!!")
              | Some c -> c) in 
           let action = 
-            P.Maction([("actiontype","toggle")],
+            P.Maction([None,"actiontype","toggle"],
               [(make_concl "proof of" ac);
                 body]) in
-          P.Mtable ([("align","baseline 1");("equalrows","false");
-              ("columnalign","left")],
+          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+              None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
              P.Mtr ([],[P.Mtd ([], P.indented action)])])
 
@@ -227,8 +227,8 @@ and proof2pres term2pres p =
     let module P = Mpresentation in
     List.fold_right
       (fun ce continuation ->
-         P.Mtable([("align","baseline 1");("equalrows","false");
-          ("columnalign","left")],
+         P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
+          None,"columnalign","left"],
            [P.Mtr([],[P.Mtd ([],ce2pres ce)]);
             P.Mtr([],[P.Mtd ([], continuation)])])) c continuation
 
@@ -246,8 +246,8 @@ and proof2pres term2pres p =
               Some s ->
                 let ty = term2pres d.Con.dec_type in
                 P.Mrow ([],
-                  [P.Mtext([("mathcolor","Red")],"Assume");
-                   P.Mspace([("width","0.1cm")]);
+                  [P.Mtext([None,"mathcolor","Red"],"Assume");
+                   P.Mspace([None,"width","0.1cm"]);
                    P.Mi([],s);
                    P.Mtext([],":");
                    ty])
@@ -258,12 +258,12 @@ and proof2pres term2pres p =
               Some s ->
                 let ty = term2pres h.Con.dec_type in
                 P.Mrow ([],
-                  [P.Mtext([("mathcolor","Red")],"Suppose");
-                   P.Mspace([("width","0.1cm")]);
+                  [P.Mtext([None,"mathcolor","Red"],"Suppose");
+                   P.Mspace([None,"width","0.1cm"]);
                    P.Mtext([],"(");
                    P.Mi ([],s);
                    P.Mtext([],")");
-                   P.Mspace([("width","0.1cm")]);
+                   P.Mspace([None,"width","0.1cm"]);
                    ty])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
@@ -291,8 +291,8 @@ and proof2pres term2pres p =
              P.indented (proof2pres p)
            else 
              proof2pres p in
-         P.Mtable([("align","baseline 1");("equalrows","false");
-          ("columnalign","left")],
+         P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
+          None,"columnalign","left"],
            [P.Mtr([],[P.Mtd ([],hd)]);
             P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation 
 
@@ -338,7 +338,7 @@ and proof2pres term2pres p =
            None -> P.Mtext([],"NO SYNTH!!!")
          | Some c -> (term2pres c)) in
       P.Mtable 
-        ([("align","baseline 1");("equalrows","false");("columnalign","left")],
+        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
         [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]);
          P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]);
          P.Mtr([],[P.Mtd([],proof2pres subproof)])])
@@ -358,7 +358,7 @@ and proof2pres term2pres p =
            [Con.Term t] -> term2pres t
          | _ -> assert false) in
       make_row 
-        [arg;P.Mspace([("width","0.1cm")]);P.Mtext([],"proves")] conclusion
+        [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       let conclusion = 
       (match conclude.Con.conclude_conclusion with 
@@ -367,8 +367,8 @@ and proof2pres term2pres p =
       (match conclude.Con.conclude_args with
          [Con.ArgProof p] -> 
            P.Mtable 
-            ([("align","baseline 1");("equalrows","false");
-              ("columnalign","left")],
+            ([None,"align","baseline 1"; None,"equalrows","false";
+              None,"columnalign","left"],
               [P.Mtr([],[P.Mtd([],proof2pres p)]);
                P.Mtr([],[P.Mtd([],
                 (make_concl "we proved *" conclusion))])]);
@@ -392,14 +392,14 @@ and proof2pres term2pres p =
         (match conclude.Con.conclude_conclusion with 
            None -> P.Mtext([],"NO Conclusion!!!")
          | Some c -> term2pres c) in
-      P.Mtable ([("align","baseline 1");("equalrows","false");
-            ("columnalign","left")],
+      P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
+            None,"columnalign","left"],
              [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
-               P.Mtext([("mathcolor","Red")],"rewrite");
-               P.Mspace([("width","0.1cm")]);term1;
-               P.Mspace([("width","0.1cm")]);
-               P.Mtext([("mathcolor","Red")],"with");
-               P.Mspace([("width","0.1cm")]);term2]))]);
+               P.Mtext([None,"mathcolor","Red"],"rewrite");
+               P.Mspace([None,"width","0.1cm"]);term1;
+               P.Mspace([None,"width","0.1cm"]);
+               P.Mtext([None,"mathcolor","Red"],"with");
+               P.Mspace([None,"width","0.1cm"]);term2]))]);
               P.Mtr ([],[P.Mtd ([],P.indented justif)]);
               P.Mtr ([],[P.Mtd ([],make_concl "we proved" conclusion)])])
     else if conclude.Con.conclude_method = "Apply" then
@@ -407,35 +407,35 @@ and proof2pres term2pres p =
         make_args_for_apply term2pres conclude.Con.conclude_args in 
       let by = 
          P.Mrow([],
-           P.Mtext([("mathcolor","Red")],"by")::P.Mspace([("width","0.1cm")])::
+           P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
            P.Mo([],"(")::pres_args@[P.Mo([],")")]) in 
       match conclude.Con.conclude_conclusion with
         None -> P.Mrow([],[P.Mtext([],"QUA");by])
       | Some t ->
          let concl = (term2pres t) in
          let ann_concl = make_concl "we proved" concl in
-         P.Mtable ([("align","baseline 1");("equalrows","false");
-            ("columnalign","left")],
+         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+            None,"columnalign","left"],
              [P.Mtr ([],[P.Mtd ([],by)]);
               P.Mtr ([],[P.Mtd ([],ann_concl)])])
     else let body =
       P.Mtable 
-        ([("align","baseline 1");("equalrows","false");("columnalign","left")],
+        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
          [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]);
           P.Mtr ([],
            [P.Mtd ([], 
              (P.indented 
                (P.Mtable 
-                 ([("align","baseline 1");("equalrows","false");
-                   ("columnalign","left")],
+                 ([None,"align","baseline 1"; None,"equalrows","false";
+                   None,"columnalign","left"],
                   args2pres conclude.Con.conclude_args))))])]) in
      match conclude.Con.conclude_conclusion with
        None -> body
      | Some t ->
          let concl = (term2pres t) in
          let ann_concl = make_concl "we proved" concl in
-         P.Mtable ([("align","baseline 1");("equalrows","false");
-            ("columnalign","left")],
+         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+            None,"columnalign","left"],
              [P.Mtr ([],[P.Mtd ([],body)]);
               P.Mtr ([],[P.Mtd ([],ann_concl)])])
 
@@ -494,7 +494,7 @@ and proof2pres term2pres p =
      let we_proved = 
         (make_concl "we proved" proof_conclusion) in
      P.Mtable 
-       ([("align","baseline 1");("equalrows","false");("columnalign","left")],
+       ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
           P.Mtr ([],[P.Mtd ([],induction_on)])::
           P.Mtr ([],[P.Mtd ([],to_prove)])::
           (make_cases args_for_cases) @
@@ -530,7 +530,7 @@ and proof2pres term2pres p =
                            (match h.Con.dec_name with
                               None -> "NO NAME???"
                            | Some n ->n) in
-                         [P.Mspace([("width","0.1cm")]);
+                         [P.Mspace([None,"width","0.1cm"]);
                           P.Mi ([],name);
                           P.Mtext([],":");
                           (term2pres h.Con.dec_type)]
@@ -538,8 +538,8 @@ and proof2pres term2pres p =
                   dec@p) args [] in
           let pattern = 
             P.Mtr ([],[P.Mtd ([],P.Mrow([],
-               P.Mtext([],"Case")::P.Mspace([("width","0.1cm")])::name::pattern_aux@
-                [P.Mspace([("width","0.1cm")]);
+               P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@
+                [P.Mspace([None,"width","0.1cm"]);
                  P.Mtext([],"->")]))]) in
           let subconcl = 
             (match p.Con.proof_conclude.Con.conclude_conclusion with
@@ -566,7 +566,7 @@ and proof2pres term2pres p =
                        [P.Mtext([],"(");
                         P.Mi ([],name);
                         P.Mtext([],")");
-                        P.Mspace([("width","0.1cm")]);
+                        P.Mspace([None,"width","0.1cm"]);
                         term2pres h.Con.dec_type]))
                    | _ -> assert false in
                let hyps = 
@@ -579,8 +579,8 @@ and proof2pres term2pres p =
           let body = conclude2pres p.Con.proof_conclude true in
           let presacontext = 
             acontext2pres p.Con.proof_apply_context body true in
-          P.Mtable ([("align","baseline 1");("equalrows","false");
-             ("columnalign","left")],
+          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+             None,"columnalign","left"],
              pattern::asubconcl::induction_hypothesis@
               [P.Mtr([],[P.Mtd([],presacontext)])])
       | _ -> assert false in