termEditor.cmo: disambiguate.cmi termEditor.cmi
termEditor.cmx: disambiguate.cmx termEditor.cmi
termEditor.cmi: disambiguate.cmi
-gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \
- mQueryGenerator.cmi mQueryLevels.cmi mQueryLevels2.cmi misc.cmi \
- proofEngine.cmi sequentPp.cmi termEditor.cmi xml2Gdome.cmi
-gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \
- mQueryGenerator.cmx mQueryLevels.cmx mQueryLevels2.cmx misc.cmx \
- proofEngine.cmx sequentPp.cmx termEditor.cmx xml2Gdome.cmx
+applyStylesheets.cmo: misc.cmi applyStylesheets.cmi
+applyStylesheets.cmx: misc.cmx applyStylesheets.cmi
+invokeTactics.cmo: cic2acic.cmi logicalOperations.cmi misc.cmi \
+ proofEngine.cmi sequentPp.cmi termEditor.cmi xml2Gdome.cmi \
+ invokeTactics.cmi
+invokeTactics.cmx: cic2acic.cmx logicalOperations.cmx misc.cmx \
+ proofEngine.cmx sequentPp.cmx termEditor.cmx xml2Gdome.cmx \
+ invokeTactics.cmi
+invokeTactics.cmi: cic2acic.cmi termEditor.cmi
+gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi \
+ logicalOperations.cmi mQueryGenerator.cmi mQueryLevels.cmi \
+ mQueryLevels2.cmi misc.cmi proofEngine.cmi sequentPp.cmi termEditor.cmi \
+ xml2Gdome.cmi
+gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx \
+ logicalOperations.cmx mQueryGenerator.cmx mQueryLevels.cmx \
+ mQueryLevels2.cmx misc.cmx proofEngine.cmx sequentPp.cmx termEditor.cmx \
+ xml2Gdome.cmx
sequentPp.ml sequentPp.mli mQueryGenerator.mli mQueryLevels.ml \
mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \
disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \
- gTopLevel.ml
+ applyStylesheets.ml applyStylesheets.mli gTopLevel.ml
TOPLEVELOBJS = \
xml2Gdome.cmo proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \
cic2Xml.cmo logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \
mQueryLevels2.cmo mQueryGenerator.cmo misc.cmo disambiguate.cmo \
- termEditor.cmo gTopLevel.cmo
+ termEditor.cmo applyStylesheets.cmo gTopLevel.cmo
depend:
$(OCAMLDEP) $(DEPOBJS) > .depend
--- /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/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 30/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+let parseStyle name =
+ let style =
+ Misc.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 apply_stylesheets input styles args =
+ List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
+ input styles
+;;
+
+let apply_proof_stylesheets proof_doc ~explode_all =
+ apply_stylesheets proof_doc mml_styles (mml_args ~explode_all)
+;;
+
+let apply_sequent_stylesheets sequent_doc =
+ apply_stylesheets sequent_doc sequent_styles sequent_args
+;;
--- /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/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 15/01/2003 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+val apply_proof_stylesheets :
+ Gdome.document -> explode_all:bool -> Gdome.document
+val apply_sequent_stylesheets : Gdome.document -> Gdome.document
(* 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)
baseuri ^ "#" ^ rest
with Not_found -> uri
;;
+
+let domImpl = Gdome.domImplementation ();;
+let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
(* *)
(******************************************************************************)
-(** Functions that should be moved in another module **)
exception IllFormedUri of string
val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
+
+val domImpl : Gdome.domImplementation
+val helmns : Gdome.domString
projects / helm.git / commitdiff