(* GLOBAL CONSTANTS *)
-let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
let htmlheader =
function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
;;
-let domImpl = Gdome.domImplementation ();;
-
-let parseStyle name =
- let style =
- domImpl#createDocumentFromURI
-(*
- ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
-*)
- ~uri:("styles/" ^ name) ()
- in
- Gdome_xslt.processStylesheet style
-;;
-
-let d_c = parseStyle "drop_coercions.xsl";;
-let tc1 = parseStyle "objtheorycontent.xsl";;
-let hc2 = parseStyle "content_to_html.xsl";;
-let l = parseStyle "link.xsl";;
-
-let c1 = parseStyle "rootcontent.xsl";;
-let g = parseStyle "genmmlid.xsl";;
-let c2 = parseStyle "annotatedpres.xsl";;
-
-
-let getterURL = Configuration.getter_url;;
-let processorURL = Configuration.processor_url;;
-
-let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
-let mml_args ~explode_all =
- ("explodeall",(if explode_all then "true()" else "false()"))::
- ["processorURL", "'" ^ processorURL ^ "'" ;
- "getterURL", "'" ^ getterURL ^ "'" ;
- "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
- "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
- "UNICODEvsSYMBOL", "'symbol'" ;
- "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
- "encoding", "'iso-8859-1'" ;
- "media-type", "'text/html'" ;
- "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
- "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
- "naturalLanguage", "'yes'" ;
- "annotations", "'no'" ;
- "URLs_or_URIs", "'URIs'" ;
- "topurl", "'http://phd.cs.unibo.it/helm'" ;
- "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
-;;
-
-let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
-let sequent_args =
- ["processorURL", "'" ^ processorURL ^ "'" ;
- "getterURL", "'" ^ getterURL ^ "'" ;
- "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
- "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
- "UNICODEvsSYMBOL", "'symbol'" ;
- "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
- "encoding", "'iso-8859-1'" ;
- "media-type", "'text/html'" ;
- "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
- "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
- "naturalLanguage", "'no'" ;
- "annotations", "'no'" ;
- "explodeall", "true()" ;
- "URLs_or_URIs", "'URIs'" ;
- "topurl", "'http://phd.cs.unibo.it/helm'" ;
- "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
-;;
-
-let parse_file filename =
- let inch = open_in filename in
- let rec read_lines () =
- try
- let line = input_line inch in
- line ^ read_lines ()
- with
- End_of_file -> ""
- in
- read_lines ()
-;;
-
-let applyStylesheets input styles args =
- List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
- input styles
-;;
-
let
mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
=
in
let input =
match bodyxml with
- None -> Xml2Gdome.document_of_xml domImpl xml
+ None -> Xml2Gdome.document_of_xml Misc.domImpl xml
| Some bodyxml' ->
Xml.pp xml (Some constanttypefile) ;
- Xml2Gdome.document_of_xml domImpl bodyxml'
+ Xml2Gdome.document_of_xml Misc.domImpl bodyxml'
in
(*CSC: We save the innertypes to disk so that we can retrieve them in the *)
(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
(*CSC: local. *)
Xml.pp xmlinnertypes (Some innertypesfile) ;
- let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
+ let output = ApplyStylesheets.apply_proof_stylesheets input ~explode_all in
output
;;
end
else
begin
- let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
+ let sequent_doc =
+ Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
let sequent_mml =
- applyStylesheets sequent_doc sequent_styles sequent_args
+ ApplyStylesheets.apply_sequent_stylesheets sequent_doc
in
notebook#set_current_page ~may_skip_switch_page_event:true metano;
notebook#proofw#load_doc ~dom:sequent_mml
SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
in
let sequent_doc =
- Xml2Gdome.document_of_xml domImpl sequent_gdome
+ Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome
in
- let res =
- applyStylesheets sequent_doc sequent_styles sequent_args ;
- in
+ let res = ApplyStylesheets.apply_sequent_stylesheets sequent_doc in
current_scratch_infos :=
Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
res
(*CSC: OCAML DIVERGE
((element : G.element)#getAttributeNS
*)
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
(*CSC: OCAML DIVERGE
((element : G.element)#getAttributeNS
*)
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
[node] ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
let term_of_node node =
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
[node] ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
[node] ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
let term_of_node node =
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
[node] ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
let module G = Gdome in
let rec aux element =
if element#hasAttributeNS
- ~namespaceURI:helmns
+ ~namespaceURI:Misc.helmns
~localName:(G.domString "xref")
then
mmlwidget#set_selection (Some element)
projects / helm.git / blobdiff