From 6f65a2e518d723ea722b23bfd9fa0162ff8be457 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 Jul 2003 22:46:22 +0000 Subject: [PATCH] Xml.token is now namespace-aware. As a consequence, xml2Gdomexmath is no longer needed. (It was a terrible hack indeed). --- helm/gTopLevel/termViewer.ml | 20 ++- .../cic_annotations/cicAnnotation2Xml.ml | 4 +- helm/ocaml/cic_transformations/.depend | 2 - helm/ocaml/cic_transformations/Makefile | 2 +- helm/ocaml/cic_transformations/cexpr2pres.ml | 60 ++++----- helm/ocaml/cic_transformations/cexpr2pres.mli | 8 +- helm/ocaml/cic_transformations/cic2Xml.ml | 111 +++++++++-------- .../ocaml/cic_transformations/content2pres.ml | 98 +++++++-------- .../cic_transformations/mpresentation.ml | 92 +++++++------- .../cic_transformations/mpresentation.mli | 12 +- helm/ocaml/cic_transformations/sequentPp.ml | 7 +- helm/ocaml/cic_transformations/xml2Gdome.ml | 116 ++++++++++++++---- .../cic_transformations/xml2Gdomexmath.ml | 111 ----------------- .../cic_transformations/xml2Gdomexmath.mli | 27 ---- helm/ocaml/xml/xml.ml | 47 ++++--- helm/ocaml/xml/xml.mli | 27 ++-- 16 files changed, 343 insertions(+), 401 deletions(-) delete mode 100644 helm/ocaml/cic_transformations/xml2Gdomexmath.ml delete mode 100644 helm/ocaml/cic_transformations/xml2Gdomexmath.mli diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 192bbb413..5291c3587 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -33,7 +33,7 @@ (* *) (******************************************************************************) -let use_stylesheets = ref true;;(* false performs the transformations in OCaml*) +let use_stylesheets = ref false;;(* false performs the transformations in OCaml*) (* List utility functions *) exception Skip;; @@ -210,9 +210,8 @@ class proof_viewer obj = Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> let time1 = Sys.time () in let content = - Cic2content.acic2content - (ref 0) ~name:(Some "prova") ~ids_to_inner_sorts - ~ids_to_inner_types bo in + Cic2content.acic2content + (ref 0) ~name:(Some "prova") ~ids_to_inner_sorts ~ids_to_inner_types bo in let content2pres = (Content2pres.proof2pres (function p -> @@ -221,12 +220,7 @@ class proof_viewer obj = let pres = content2pres content in let time2 = Sys.time () in (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) - let xmlpres = - Xml.xml_nempty "math" - ["xmlns","http://www.w3.org/1998/Math/MathML" ; - "xmlns:helm","http://www.cs.unibo.it/helm" ; - "xmlns:xlink","http://www.w3.org/1999/xlink" - ] (Mpresentation.print_mpres pres) in + let xmlpres = Mpresentation.print_mpres pres in let time25 = Sys.time () in (* prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); @@ -235,11 +229,11 @@ class proof_viewer obj = prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25))); *) (try - (* prerr_endline "(******** INIZIO DOM **********)"; *) - let mml = Xml2Gdomexmath.document_of_xml Misc.domImpl xmlpres in + prerr_endline "(******** INIZIO DOM **********)"; + let mml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in let time3 = Sys.time () in (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *) - (* prerr_endline "(******** FINE DOM **********)"; *) + prerr_endline "(******** FINE DOM **********)"; self#load_doc ~dom:mml; prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2))) (* diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index 353ef1f74..23c3a9b68 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -38,7 +38,7 @@ let print_ann i2a id = let ann = get_ann i2a id in match ann with None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + | Some ann -> (X.xml_nempty "Annotation" [None,"of", id] (X.xml_cdata ann)) ;; (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) @@ -106,7 +106,7 @@ let pp_annotation obj i2a curi = [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Annotations" - ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] + [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] begin match obj with C.AConstant (xid, xidobj, _, te, ty, _) -> diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 2640418cd..11e89e6cb 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -33,8 +33,6 @@ misc.cmo: misc.cmi misc.cmx: misc.cmi xml2Gdome.cmo: xml2Gdome.cmi xml2Gdome.cmx: xml2Gdome.cmi -xml2Gdomexmath.cmo: xml2Gdomexmath.cmi -xml2Gdomexmath.cmx: xml2Gdomexmath.cmi sequentPp.cmo: cic2Xml.cmi cic2acic.cmi sequentPp.cmi sequentPp.cmx: cic2Xml.cmx cic2acic.cmx sequentPp.cmi applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index dae324ab3..76470873b 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -6,7 +6,7 @@ INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli cic2Xml.mli \ cic2content.mli content_expressions.mli contentPp.mli \ mpresentation.mli cexpr2pres.mli content2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli \ - xml2Gdomexmath.mli sequentPp.mli applyStylesheets.mli + sequentPp.mli applyStylesheets.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = 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 [] -> [] diff --git a/helm/ocaml/cic_transformations/cexpr2pres.mli b/helm/ocaml/cic_transformations/cexpr2pres.mli index 968e9a9cc..2bdba9e4d 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres.mli +++ b/helm/ocaml/cic_transformations/cexpr2pres.mli @@ -38,8 +38,8 @@ val symbol_table : priority:int -> assoc:bool -> tail:Mpresentation.mpres list -> - (string * string) list -> - (string * string) list -> + (string option * string * string) list -> + (string option * string * string) list -> Mpresentation.mpres ) Hashtbl.t @@ -49,8 +49,8 @@ val symbol_table_charcount : priority:int -> assoc:bool -> tail:Mpresentation.mpres list -> - (string * string) list -> - (string * string) list -> + (string option * string * string) list -> + (string option * string * string) list -> Mpresentation.mpres ) Hashtbl.t diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 564493cb8..d945cc82f 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -49,16 +49,18 @@ let print_term ~ids_to_inner_sorts = C.ARel (id,idref,n,b) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_empty "REL" - ["value",(string_of_int n) ; "binder",b ; "id",id ; "idref",idref ; - "sort",sort] + [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ; + None,"idref",idref ; None,"sort",sort] | C.AVar (id,uri,exp_named_subst) -> let sort = Hashtbl.find ids_to_inner_sorts id in aux_subst uri - (X.xml_empty "VAR" ["uri",U.string_of_uri uri;"id",id;"sort",sort]) + (X.xml_empty "VAR" + [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort]) exp_named_subst | C.AMeta (id,n,l) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort] + X.xml_nempty "META" + [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort] (List.fold_left (fun i t -> match t with @@ -74,7 +76,7 @@ let print_term ~ids_to_inner_sorts = | C.Set -> "Set" | C.Type -> "Type" in - X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id] + X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id] | C.AImplicit _ -> raise NotImplemented | C.AProd (last_id,_,_,_) as prods -> let rec eat_prods = @@ -86,17 +88,17 @@ let print_term ~ids_to_inner_sorts = in let prods,t = eat_prods prods in let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "PROD" ["type",sort] + X.xml_nempty "PROD" [None,"type",sort] [< List.fold_left (fun i (id,binder,s) -> let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in let attrs = - ("id",id)::("type",sort):: + (None,"id",id)::(None,"type",sort):: match binder with C.Anonymous -> [] - | C.Name b -> ["binder",b] + | C.Name b -> [None,"binder",b] in [< i ; X.xml_nempty "decl" attrs (aux s) >] ) [< >] prods ; @@ -104,7 +106,7 @@ let print_term ~ids_to_inner_sorts = >] | C.ACast (id,v,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "CAST" ["id",id ; "sort",sort] + X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort] [< X.xml_nempty "term" [] (aux v) ; X.xml_nempty "type" [] (aux t) >] @@ -118,17 +120,17 @@ let print_term ~ids_to_inner_sorts = in let lambdas,t = eat_lambdas lambdas in let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LAMBDA" ["sort",sort] + X.xml_nempty "LAMBDA" [None,"sort",sort] [< List.fold_left (fun i (id,binder,s) -> let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in let attrs = - ("id",id)::("type",sort):: + (None,"id",id)::(None,"type",sort):: match binder with C.Anonymous -> [] - | C.Name b -> ["binder",b] + | C.Name b -> [None,"binder",b] in [< i ; X.xml_nempty "decl" attrs (aux s) >] ) [< >] lambdas ; @@ -146,15 +148,15 @@ let print_term ~ids_to_inner_sorts = in let letins,t = eat_letins letins in let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LETIN" ["sort",sort] + X.xml_nempty "LETIN" [None,"sort",sort] [< List.fold_left (fun i (id,binder,s) -> let sort = Hashtbl.find ids_to_inner_sorts id in let attrs = - ("id",id)::("sort",sort):: + (None,"id",id)::(None,"sort",sort):: match binder with C.Anonymous -> [] - | C.Name b -> ["binder",b] + | C.Name b -> [None,"binder",b] in [< i ; X.xml_nempty "def" attrs (aux s) >] ) [< >] letins ; @@ -162,36 +164,37 @@ let print_term ~ids_to_inner_sorts = >] | C.AAppl (id,li) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "APPLY" ["id",id ; "sort",sort] + X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort] [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) >] | C.AConst (id,uri,exp_named_subst) -> let sort = Hashtbl.find ids_to_inner_sorts id in aux_subst uri (X.xml_empty "CONST" - ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort] + [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort] ) exp_named_subst | C.AMutInd (id,uri,i,exp_named_subst) -> aux_subst uri (X.xml_empty "MUTIND" - ["uri", (U.string_of_uri uri) ; - "noType",(string_of_int i) ; - "id",id] + [None, "uri", (U.string_of_uri uri) ; + None, "noType", (string_of_int i) ; + None, "id", id] ) exp_named_subst | C.AMutConstruct (id,uri,i,j,exp_named_subst) -> let sort = Hashtbl.find ids_to_inner_sorts id in aux_subst uri (X.xml_empty "MUTCONSTRUCT" - ["uri", (U.string_of_uri uri) ; - "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; - "id",id ; "sort",sort] + [None,"uri", (U.string_of_uri uri) ; + None,"noType",(string_of_int i) ; + None,"noConstr",(string_of_int j) ; + None,"id",id ; None,"sort",sort] ) exp_named_subst | C.AMutCase (id,uri,typeno,ty,te,patterns) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_nempty "MUTCASE" - ["uriType",(U.string_of_uri uri) ; - "noType", (string_of_int typeno) ; - "id", id ; "sort",sort] + [None,"uriType",(U.string_of_uri uri) ; + None,"noType", (string_of_int typeno) ; + None,"id", id ; None,"sort",sort] [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; List.fold_right @@ -201,11 +204,12 @@ let print_term ~ids_to_inner_sorts = | C.AFix (id, no, funs) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_nempty "FIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right (fun (id,fi,ai,ti,bi) i -> [< X.xml_nempty "FixFunction" - ["id",id ; "name", fi ; "recIndex", (string_of_int ai)] + [None,"id",id ; None,"name", fi ; + None,"recIndex", (string_of_int ai)] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] >] ; @@ -216,10 +220,10 @@ let print_term ~ids_to_inner_sorts = | C.ACoFix (id,no,funs) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_nempty "COFIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right (fun (id,fi,ti,bi) i -> - [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi] + [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] >] ; @@ -234,7 +238,7 @@ let print_term ~ids_to_inner_sorts = target else Xml.xml_nempty "instantiate" - (match id with None -> [] | Some id -> ["id",id]) + (match id with None -> [] | Some id -> [None,"id",id]) [< target ; List.fold_left (fun i (uri,arg) -> @@ -253,7 +257,7 @@ let print_term ~ids_to_inner_sorts = in find_relUri buri_frags uri_frags in - [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >] + [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >] ) [<>] subst >] in @@ -272,28 +276,30 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = (*CSC: Should the CurrentProof also have the list of variables it depends on? *) (*CSC: I think so. Not implemented yet. *) X.xml_nempty "CurrentProof" - ["of",UriManager.string_of_uri uri ; "id", id] + [None,"of",UriManager.string_of_uri uri ; None,"id", id] [< List.fold_left (fun i (cid,n,canonical_context,t) -> [< i ; X.xml_nempty "Conjecture" - ["id", cid ; "no",(string_of_int n)] + [None,"id",cid ; None,"no",(string_of_int n)] [< List.fold_left (fun i (hid,t) -> [< (match t with Some (n,C.ADecl t) -> X.xml_nempty "Decl" (match n with - C.Name n' -> ["id",hid;"name",n'] - | C.Anonymous -> ["id",hid]) + C.Name n' -> + [None,"id",hid;None,"name",n'] + | C.Anonymous -> [None,"id",hid]) (print_term ids_to_inner_sorts t) | Some (n,C.ADef t) -> X.xml_nempty "Def" (match n with - C.Name n' -> ["id",hid;"name",n'] - | C.Anonymous -> ["id",hid]) + C.Name n' -> + [None,"id",hid;None,"name",n'] + | C.Anonymous -> [None,"id",hid]) (print_term ids_to_inner_sorts t) - | None -> X.xml_empty "Hidden" ["id",hid] + | None -> X.xml_empty "Hidden" [None,"id",hid] ) ; i >] @@ -306,7 +312,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] in let xml_for_current_proof_type = - X.xml_nempty "ConstantType" ["name",n ; "params",params' ; "id", id] + X.xml_nempty "ConstantType" + [None,"name",n ; None,"params",params' ; None,"id", id] (print_term ids_to_inner_sorts ty) in let xmlbo = @@ -333,8 +340,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n") ; X.xml_nempty "ConstantBody" - ["for",UriManager.string_of_uri uri ; "params",params' ; - "id", id] + [None,"for",UriManager.string_of_uri uri ; + None,"params",params' ; None,"id", id] [< print_term ids_to_inner_sorts bo >] >] in @@ -342,7 +349,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [< X.xml_cdata "\n" ; X.xml_cdata ("\n"); X.xml_nempty "ConstantType" - ["name",n ; "params",params' ; "id", id] + [None,"name",n ; None,"params",params' ; None,"id", id] [< print_term ids_to_inner_sorts ty >] >] in @@ -359,7 +366,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [< X.xml_cdata "\n" ; X.xml_cdata ("\n"); X.xml_nempty "Variable" - ["name",n ; "params",params' ; "id", id] + [None,"name",n ; None,"params",params' ; None,"id", id] [< xmlbo ; X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) >] @@ -372,15 +379,15 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n") ; X.xml_nempty "InductiveDefinition" - ["noParams",string_of_int nparams ; - "id",id ; - "params",params'] + [None,"noParams",string_of_int nparams ; + None,"id",id ; + None,"params",params'] [< (List.fold_left (fun i (id,typename,finite,arity,cons) -> [< i ; X.xml_nempty "InductiveType" - ["id",id ; "name",typename ; - "inductive",(string_of_bool finite) + [None,"id",id ; None,"name",typename ; + None,"inductive",(string_of_bool finite) ] [< X.xml_nempty "arity" [] (print_term ids_to_inner_sorts arity) ; @@ -388,7 +395,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = (fun i (name,lc) -> [< i ; X.xml_nempty "Constructor" - ["name",name] + [None,"name",name] (print_term ids_to_inner_sorts lc) >]) [<>] cons ) @@ -410,11 +417,11 @@ let [< X.xml_cdata "\n" ; X.xml_cdata ("\n") ; - X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi] + X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi] (Hashtbl.fold (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> [< x ; - X.xml_nempty "TYPE" ["of",id] + X.xml_nempty "TYPE" [None,"of",id] [< X.xml_nempty "synthesized" [] [< print_term ids_to_inner_sorts synty >] ; match expty with diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 019538169..5d6923237 100644 --- 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 diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 116b845b5..de1172d2a 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -66,28 +66,22 @@ type (* Enlivening Expressions *) | Maction of attr * mpres list -and +and row = Mtr of attr * mtd list - row = Mtr of attr * mtd list - -and - - mtd = Mtd of attr * mpres - -and - - attr = (string * string) list +and mtd = Mtd of attr * mpres +and attr = (string option * string * string) list ;; -let smallskip = Mspace([("width","0.1cm")]);; -let indentation = Mspace([("width","0.3cm")]);; +let smallskip = Mspace([None,"width","0.1cm"]);; +let indentation = Mspace([None,"width","0.3cm"]);; let indented elem = Mrow([],[indentation;elem]);; let standard_tbl_attr = - [("align","baseline 1");("equalrows","false");("columnalign","left")];; + [None,"align","baseline 1";None,"equalrows","false";None,"columnalign","left"] +;; let two_rows_table attr a b = Mtable(attr@standard_tbl_attr, @@ -112,77 +106,80 @@ let row_with_brackets attr a b op = let row_without_brackets attr a b op = Mrow(attr,[a;smallskip;op;smallskip;b]) + +(* MathML prefix *) +let prefix = "m";; let rec print_mpres = let module X = Xml in - function - Mi (attr,s) -> X.xml_nempty "mi" attr (X.xml_cdata s) - | Mn (attr,s) -> X.xml_nempty "mn" attr (X.xml_cdata s) - | Mo (attr,s) -> X.xml_nempty "mo" attr (X.xml_cdata s) - | Mtext (attr,s) -> X.xml_nempty "mtext" attr (X.xml_cdata s) - | Mspace attr -> X.xml_empty "mspace" attr - | Ms (attr,s) -> X.xml_nempty "ms" attr (X.xml_cdata s) - | Mgliph (attr,s) -> X.xml_nempty "mgliph" attr (X.xml_cdata s) + function + Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s) + | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s) + | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s) + | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s) + | Mspace attr -> X.xml_empty ~prefix "mspace" attr + | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s) + | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s) (* General Layout Schemata *) | Mrow (attr,l) -> - X.xml_nempty "mrow" attr + X.xml_nempty ~prefix "mrow" attr [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) >] | Mfrac (attr,m1,m2) -> - X.xml_nempty "mfrac" attr + X.xml_nempty ~prefix "mfrac" attr [< print_mpres m1; print_mpres m2 >] | Msqrt (attr,m) -> - X.xml_nempty "msqrt" attr [< print_mpres m >] + X.xml_nempty ~prefix "msqrt" attr [< print_mpres m >] | Mroot (attr,m1,m2) -> - X.xml_nempty "mroot" attr + X.xml_nempty ~prefix "mroot" attr [< print_mpres m1; print_mpres m2 >] | Mstyle (attr,m) -> - X.xml_nempty "mstyle" attr [< print_mpres m >] + X.xml_nempty ~prefix "mstyle" attr [< print_mpres m >] | Merror (attr,m) -> - X.xml_nempty "merror" attr [< print_mpres m >] + X.xml_nempty ~prefix "merror" attr [< print_mpres m >] | Mpadded (attr,m) -> - X.xml_nempty "mpadded" attr [< print_mpres m >] + X.xml_nempty ~prefix "mpadded" attr [< print_mpres m >] | Mphantom (attr,m) -> - X.xml_nempty "mphantom" attr [< print_mpres m >] + X.xml_nempty ~prefix "mphantom" attr [< print_mpres m >] | Mfenced (attr,l) -> - X.xml_nempty "mfenced" attr + X.xml_nempty ~prefix "mfenced" attr [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) >] | Menclose (attr,m) -> - X.xml_nempty "menclose" attr [< print_mpres m >] + X.xml_nempty ~prefix "menclose" attr [< print_mpres m >] (* Script and Limit Schemata *) | Msub (attr,m1,m2) -> - X.xml_nempty "msub" attr + X.xml_nempty ~prefix "msub" attr [< print_mpres m1; print_mpres m2 >] | Msup (attr,m1,m2) -> - X.xml_nempty "msup" attr + X.xml_nempty ~prefix "msup" attr [< print_mpres m1; print_mpres m2 >] | Msubsup (attr,m1,m2,m3) -> - X.xml_nempty "msubsup" attr + X.xml_nempty ~prefix "msubsup" attr [< print_mpres m1; print_mpres m2; print_mpres m3 >] | Munder (attr,m1,m2) -> - X.xml_nempty "munder" attr + X.xml_nempty ~prefix "munder" attr [< print_mpres m1; print_mpres m2 >] | Mover (attr,m1,m2) -> - X.xml_nempty "mover" attr + X.xml_nempty ~prefix "mover" attr [< print_mpres m1; print_mpres m2 >] | Munderover (attr,m1,m2,m3) -> - X.xml_nempty "munderover" attr + X.xml_nempty ~prefix "munderover" attr [< print_mpres m1; print_mpres m2; print_mpres m3 @@ -190,12 +187,12 @@ let rec print_mpres = (* | Multiscripts of ??? NOT IMPLEMEMENTED *) (* Tables and Matrices *) | Mtable (attr, rl) -> - X.xml_nempty "mtable" attr + X.xml_nempty ~prefix "mtable" attr [< (List.fold_right (fun x i -> [< (print_mrow x) ; i >]) rl [<>]) >] (* Enlivening Expressions *) | Maction (attr, l) -> - X.xml_nempty "maction" attr + X.xml_nempty ~prefix "maction" attr [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) >] @@ -203,16 +200,23 @@ and print_mrow = let module X = Xml in function Mtr (attr, l) -> - X.xml_nempty "mtr" attr + X.xml_nempty ~prefix "mtr" attr [< (List.fold_right (fun x i -> [< (print_mtd x) ; i >]) l [<>]) >] and print_mtd = let module X = Xml in function - Mtd (attr,m) -> X.xml_nempty "mtd" attr (print_mpres m) + Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr (print_mpres m) ;; - - - +let print_mpres pres = + [< Xml.xml_cdata "\n" ; + Xml.xml_cdata "\n"; + Xml.xml_nempty ~prefix "math" + [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ; + Some "xmlns","helm","http://www.cs.unibo.it/helm" ; + Some "xmlns","xlink","http://www.w3.org/1999/xlink" + ] (print_mpres pres) + >] +;; diff --git a/helm/ocaml/cic_transformations/mpresentation.mli b/helm/ocaml/cic_transformations/mpresentation.mli index 53eb9927e..53df1fb1d 100644 --- a/helm/ocaml/cic_transformations/mpresentation.mli +++ b/helm/ocaml/cic_transformations/mpresentation.mli @@ -57,17 +57,11 @@ type (* Enlivening Expressions *) | Maction of attr * mpres list -and +and row = Mtr of attr * mtd list - row = Mtr of attr * mtd list +and mtd = Mtd of attr * mpres -and - - mtd = Mtd of attr * mpres - -and - - attr = (string * string) list +and attr = (string option * string * string) list ;; diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml index 8cce6e1e3..bda66841c 100644 --- a/helm/ocaml/cic_transformations/sequentPp.ml +++ b/helm/ocaml/cic_transformations/sequentPp.ml @@ -90,8 +90,8 @@ module XmlPp = [< s ; X.xml_nempty (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def") - ["name",(match n with Cic.Name n -> n | _ -> assert false); - "id",hid] + [None,"name",(match n with Cic.Name n -> n | _ -> assert false); + None,"id",hid] (Cic2Xml.print_term ~ids_to_inner_sorts acic) >], (entry::context), (hid::idrefs) | None -> @@ -103,7 +103,8 @@ module XmlPp = let acic = acic_of_cic_context context final_idrefs goal None in [< X.xml_cdata "\n" ; X.xml_cdata ("\n"); - X.xml_nempty "Sequent" ["no",string_of_int metano;"id",sequent_id] + X.xml_nempty "Sequent" + [None,"no",string_of_int metano;None,"id",sequent_id] [< final_s ; Xml.xml_nempty "Goal" [] (Cic2Xml.print_term ~ids_to_inner_sorts acic) diff --git a/helm/ocaml/cic_transformations/xml2Gdome.ml b/helm/ocaml/cic_transformations/xml2Gdome.ml index c4e9445eb..3d07bf21c 100644 --- a/helm/ocaml/cic_transformations/xml2Gdome.ml +++ b/helm/ocaml/cic_transformations/xml2Gdome.ml @@ -26,46 +26,108 @@ let document_of_xml (domImplementation : Gdome.domImplementation) strm = let module G = Gdome in let module X = Xml in - let root_name,root_attributes,root_content = + let rec update_namespaces ((defaultns,bindings) as namespaces) = + function + [] -> namespaces + | (None,"xmlns",value)::tl -> + update_namespaces (Some (Gdome.domString value),bindings) tl + | (prefix,name,value)::tl when prefix = Some "xmlns" -> + update_namespaces (defaultns,(name,Gdome.domString value)::bindings) tl + | _::tl -> update_namespaces namespaces tl in + let rec namespace_of_prefix (defaultns,bindings) = + function + None -> None + | Some "xmlns" -> Some (Gdome.domString "xml-ns") + | Some p' -> + try + Some (List.assoc p' bindings) + with + Not_found -> + raise + (Failure ("The prefix " ^ p' ^ " is not bound to any namespace")) in + let get_qualified_name p n = + match p with + None -> Gdome.domString n + | Some p' -> Gdome.domString (p' ^ ":" ^ n) in + let root_prefix,root_name,root_attributes,root_content = ignore (Stream.next strm) ; (* to skip the declaration *) ignore (Stream.next strm) ; (* to skip the DOCTYPE declaration *) match Stream.next strm with - X.Empty(n,l) -> n,l,[<>] - | X.NEmpty(n,l,c) -> n,l,c + X.Empty(p,n,l) -> p,n,l,[<>] + | X.NEmpty(p,n,l,c) -> p,n,l,c | _ -> assert false in + let namespaces = update_namespaces (None,[]) root_attributes in + let namespaceURI = namespace_of_prefix namespaces root_prefix in let document = - domImplementation#createDocument ~namespaceURI:None - ~qualifiedName:(Gdome.domString root_name) ~doctype:None + domImplementation#createDocument ~namespaceURI + ~qualifiedName:(get_qualified_name root_prefix root_name) + ~doctype:None in - let rec aux (node : Gdome.node) = + let rec aux namespaces (node : Gdome.node) = parser [< 'X.Str a ; s >] -> let textnode = document#createTextNode ~data:(Gdome.domString a) in ignore (node#appendChild ~newChild:(textnode :> Gdome.node)) ; - aux node s - | [< 'X.Empty(n,l) ; s >] -> - let element = document#createElement ~tagName:(Gdome.domString n) in - List.iter (function (n,v) -> element#setAttribute - ~name:(Gdome.domString n) ~value:(Gdome.domString v)) l ; - ignore - (node#appendChild ~newChild:(element : Gdome.element :> Gdome.node)) ; - aux node s - | [< 'X.NEmpty(n,l,c) ; s >] -> - let element = document#createElement ~tagName:(Gdome.domString n) in - List.iter - (function (n,v) -> - element#setAttribute ~name:(Gdome.domString n) - ~value:(Gdome.domString v) - ) l ; - ignore (node#appendChild ~newChild:(element :> Gdome.node)) ; - aux (element :> Gdome.node) c ; - aux node s + aux namespaces node s + | [< 'X.Empty(p,n,l) ; s >] -> + let namespaces' = update_namespaces namespaces l in + let namespaceURI = namespace_of_prefix namespaces' p in + let element = + document#createElementNS ~namespaceURI + ~qualifiedName:(get_qualified_name p n) + in + List.iter + (function (p,n,v) -> + if p = None then + element#setAttribute ~name:(Gdome.domString n) + ~value:(Gdome.domString v) + else + let namespaceURI = namespace_of_prefix namespaces' p in + element#setAttributeNS + ~namespaceURI + ~qualifiedName:(get_qualified_name p n) + ~value:(Gdome.domString v) + ) l ; + ignore + (node#appendChild + ~newChild:(element : Gdome.element :> Gdome.node)) ; + aux namespaces node s + | [< 'X.NEmpty(p,n,l,c) ; s >] -> + let namespaces' = update_namespaces namespaces l in + let namespaceURI = namespace_of_prefix namespaces' p in + let element = + document#createElementNS ~namespaceURI + ~qualifiedName:(get_qualified_name p n) + in + List.iter + (function (p,n,v) -> + if p = None then + element#setAttribute ~name:(Gdome.domString n) + ~value:(Gdome.domString v) + else + let namespaceURI = namespace_of_prefix namespaces' p in + element#setAttributeNS ~namespaceURI + ~qualifiedName:(get_qualified_name p n) + ~value:(Gdome.domString v) + ) l ; + ignore (node#appendChild ~newChild:(element :> Gdome.node)) ; + aux namespaces' (element :> Gdome.node) c ; + aux namespaces node s | [< >] -> () in let root = document#get_documentElement in - List.iter (function (n,v) -> root#setAttribute - ~name:(Gdome.domString n) ~value:(Gdome.domString v)) root_attributes ; - aux (root : Gdome.element :> Gdome.node) root_content ; + List.iter + (function (p,n,v) -> + if p = None then + root#setAttribute ~name:(Gdome.domString n) + ~value:(Gdome.domString v) + else + let namespaceURI = namespace_of_prefix namespaces p in + root#setAttributeNS ~namespaceURI + ~qualifiedName:(get_qualified_name p n) + ~value:(Gdome.domString v) + ) root_attributes ; + aux namespaces (root : Gdome.element :> Gdome.node) root_content ; document ;; diff --git a/helm/ocaml/cic_transformations/xml2Gdomexmath.ml b/helm/ocaml/cic_transformations/xml2Gdomexmath.ml deleted file mode 100644 index 0b2db0d99..000000000 --- a/helm/ocaml/cic_transformations/xml2Gdomexmath.ml +++ /dev/null @@ -1,111 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* cut and paste from xml2Gdome.ml: there was the namespace problem. - This is a fst patch: we generate a fixed namespace for math *) -let document_of_xml (domImplementation : Gdome.domImplementation) strm = - let module G = Gdome in - let module X = Xml in - let namespace = "http://www.w3.org/1998/Math/MathML" in - let root_name,root_attributes,root_content = - (* - ignore (Stream.next strm) ; (* to skip the declaration *) - ignore (Stream.next strm) ; (* to skip the DOCTYPE declaration *) - *) - match Stream.next strm with - X.Empty(n,l) -> n,l,[<>] - | X.NEmpty(n,l,c) -> n,l,c - | _ -> assert false - in - let document = - domImplementation#createDocument ~namespaceURI:(Some (Gdome.domString namespace)) - ~qualifiedName:(Gdome.domString ("m:" ^ root_name)) ~doctype:None - in - document#get_documentElement#setAttribute (Gdome.domString "xmlns:m") (Gdome.domString namespace); - let rec aux (node : Gdome.node) = - parser - [< 'X.Str a ; s >] -> - let textnode = document#createTextNode ~data:(Gdome.domString a) in - ignore (node#appendChild ~newChild:(textnode :> Gdome.node)) ; - aux node s - | [< 'X.Empty(n,l) ; s >] -> - let element = document#createElementNS - ~namespaceURI:(Some (Gdome.domString namespace)) - ~qualifiedName:(Gdome.domString ("m:" ^ n)) in - List.iter - (function (n,v) -> - let i = - (try String.index n ':' - with Not_found -> 0) in - if i = 0 then - element#setAttribute - ~name:(Gdome.domString n) ~value:(Gdome.domString v) - else - let ns_label = String.sub n 0 i in - let ns = - if ns_label = "helm" then "http://www.cs.unibo.it/helm" - else if ns_label = "xlink" then "http://www.w3.org/1999/xlink" - else assert false in - element#setAttributeNS - ~namespaceURI:(Some (Gdome.domString ns)) - ~qualifiedName:(Gdome.domString n) - ~value:(Gdome.domString v)) l ; - ignore - (node#appendChild ~newChild:(element : Gdome.element :> Gdome.node)) ; - aux node s - | [< 'X.NEmpty(n,l,c) ; s >] -> - let element = document#createElementNS - ~namespaceURI:(Some (Gdome.domString namespace)) - ~qualifiedName:(Gdome.domString ("m:" ^ n)) in - List.iter - (function (n,v) -> - let i = - (try String.index n ':' - with Not_found -> 0) in - if i = 0 then - element#setAttribute - ~name:(Gdome.domString n) ~value:(Gdome.domString v) - else - let ns_label = String.sub n 0 i in - let ns = - if ns_label = "helm" then "http://www.cs.unibo.it/helm" - else if ns_label = "xlink" then "http://www.w3.org/1999/xlink" - else assert false in - element#setAttributeNS - ~namespaceURI:(Some (Gdome.domString ns)) - ~qualifiedName:(Gdome.domString n) - ~value:(Gdome.domString v)) l ; - ignore (node#appendChild ~newChild:(element :> Gdome.node)) ; - aux (element :> Gdome.node) c ; - aux node s - | [< >] -> () - in - let root = document#get_documentElement in - List.iter (function (n,v) -> root#setAttribute - ~name:(Gdome.domString n) ~value:(Gdome.domString v)) root_attributes ; - aux (root : Gdome.element :> Gdome.node) root_content ; - document -;; - diff --git a/helm/ocaml/cic_transformations/xml2Gdomexmath.mli b/helm/ocaml/cic_transformations/xml2Gdomexmath.mli deleted file mode 100644 index 45d0e9532..000000000 --- a/helm/ocaml/cic_transformations/xml2Gdomexmath.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val document_of_xml : - Gdome.domImplementation -> Xml.token Stream.t -> Gdome.document diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml index 6670e1f19..9dcd16fc0 100644 --- a/helm/ocaml/xml/xml.ml +++ b/helm/ocaml/xml/xml.ml @@ -38,44 +38,55 @@ (* the type token for XML cdata, empty elements and not-empty elements *) -(* Usage: *) -(* Str cdata *) -(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) -(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) -(* content *) -type token = Str of string - | Empty of string * (string * string) list - | NEmpty of string * (string * string) list * token Stream.t +(* Usage: *) +(* Str cdata *) +(* Empty (prefix, element_name, *) +(* [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen] *) +(* NEmpty (prefix, element_name, *) +(* [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen], *) +(* content *) +type token = + Str of string + | Empty of string option * string * (string option * string * string) list + | NEmpty of string option * string * (string option * string * string) list * + token Stream.t ;; (* currified versions of the constructors make the code more readable *) -let xml_empty name attrs = [< 'Empty(name,attrs) >] -let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >] -let xml_cdata str = [< 'Str str >] +let xml_empty ?prefix name attrs = + [< 'Empty(prefix,name,attrs) >] +let xml_nempty ?prefix name attrs content = + [< 'NEmpty(prefix,name,attrs,content) >] +let xml_cdata str = + [< 'Str str >] (** low level for other PPs: pretty print each token of strm applying 'f' to a canonical string representation of each token *) let pp_gen f strm = + let pprefix = + function + None -> "" + | Some p -> p ^ ":" in let rec pp_r m = parser | [< 'Str a ; s >] -> print_spaces m ; f (a ^ "\n") ; pp_r m s - | [< 'Empty(n,l) ; s >] -> + | [< 'Empty(p,n,l) ; s >] -> print_spaces m ; - f ("<" ^ n) ; - List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + f ("<" ^ (pprefix p) ^ n) ; + List.iter (fun (p,n,v) -> f (" " ^ (pprefix p) ^ n ^ "=\"" ^ v ^ "\"")) l; f "/>\n" ; pp_r m s - | [< 'NEmpty(n,l,c) ; s >] -> + | [< 'NEmpty(p,n,l,c) ; s >] -> print_spaces m ; - f ("<" ^ n) ; - List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + f ("<" ^ (pprefix p) ^ n) ; + List.iter (fun (p,n,v) -> f (" " ^ (pprefix p) ^ n ^ "=\"" ^ v ^ "\"")) l; f ">\n" ; pp_r (m+1) c ; print_spaces m ; - f ("\n") ; + f ("\n") ; pp_r m s | [< >] -> () and print_spaces m = diff --git a/helm/ocaml/xml/xml.mli b/helm/ocaml/xml/xml.mli index c52ae8ecd..a48e7d6b9 100644 --- a/helm/ocaml/xml/xml.mli +++ b/helm/ocaml/xml/xml.mli @@ -37,20 +37,27 @@ (******************************************************************************) (* Tokens for XML cdata, empty elements and not-empty elements *) -(* Usage: *) -(* Str cdata *) -(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) -(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) -(* content *) +(* Usage: *) +(* Str cdata *) +(* Empty (prefix, element_name, *) +(* [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen] *) +(* NEmpty (prefix, element_name, *) +(* [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen], *) +(* content *) type token = - | Str of string - | Empty of string * (string * string) list - | NEmpty of string * (string * string) list * token Stream.t + Str of string + | Empty of string option * string * (string option * string * string) list + | NEmpty of string option * string * (string option * string * string) list * + token Stream.t +;; (* currified versions of the token constructors make the code more readable *) -val xml_empty : string -> (string * string) list -> token Stream.t +val xml_empty : + ?prefix:string -> string -> (string option * string * string) list -> + token Stream.t val xml_nempty : - string -> (string * string) list -> token Stream.t -> token Stream.t + ?prefix:string -> string -> (string option * string * string) list -> + token Stream.t -> token Stream.t val xml_cdata : string -> token Stream.t (* The pretty printer for streams of token *) -- 2.39.2