no longer needed. (It was a terrible hack indeed).
(* *)
(******************************************************************************)
-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;;
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 ->
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)));
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)))
(*
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) *)
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\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, _) ->
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 \
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 =
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 =
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
(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)
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
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 ^ "="))::
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
(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
[] -> []
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
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
(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
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([],
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
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 ([],
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;
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
[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
[] -> []
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
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
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
| 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 =
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 ;
>]
| 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)
>]
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 ;
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 ;
>]
| 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
| 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 >]
>] ;
| 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 >]
>] ;
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) ->
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
(*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
>]
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 =
X.xml_cdata
("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\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
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\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
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\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)
>]
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\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) ;
(fun i (name,lc) ->
[< i ;
X.xml_nempty "Constructor"
- ["name",name]
+ [None,"name",name]
(print_term ids_to_inner_sorts lc)
>]) [<>] cons
)
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\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
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]))
;;
| 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
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
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)])])
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
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])
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)
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
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)])])
[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
(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))])]);
(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
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)])])
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) @
(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)]
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
[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 =
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
(* 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,
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
(* | 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 [<>])
>]
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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\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)
+ >]
+;;
(* 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
;;
[< 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 ->
let acic = acic_of_cic_context context final_idrefs goal None in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Sequent SYSTEM \"" ^ dtdname ^ "\">\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)
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 <?xml ...?> 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
;;
+++ /dev/null
-(* 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 <?xml ...?> 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
-;;
-
+++ /dev/null
-(* 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
(* 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 ^ ">\n") ;
+ f ("</" ^ (pprefix p) ^ n ^ ">\n") ;
pp_r m s
| [< >] -> ()
and print_spaces m =
(******************************************************************************)
(* 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 *)
projects / helm.git / commitdiff