From 7fedf47037503b281d078eef6de13927020eb410 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jan 2003 10:36:05 +0000 Subject: [PATCH] 1. helmns and domImpl moved to the misc module ;-( 2. all the constants and functions relative to stylesheet applications have been moved to the new module ApplyStylesheets, whose interface is really minimal. --- helm/gTopLevel/.depend | 23 ++++-- helm/gTopLevel/Makefile | 4 +- helm/gTopLevel/applyStylesheets.ml | 109 +++++++++++++++++++++++++ helm/gTopLevel/applyStylesheets.mli | 38 +++++++++ helm/gTopLevel/gTopLevel.ml | 119 ++++------------------------ helm/gTopLevel/misc.ml | 3 + helm/gTopLevel/misc.mli | 4 +- 7 files changed, 189 insertions(+), 111 deletions(-) create mode 100644 helm/gTopLevel/applyStylesheets.ml create mode 100644 helm/gTopLevel/applyStylesheets.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 3e72e3670..25b8f4b54 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -27,9 +27,20 @@ disambiguate.cmx: mQueryGenerator.cmx misc.cmx disambiguate.cmi 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 diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index d0210e087..c3626bcd0 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -22,13 +22,13 @@ DEPOBJS = \ 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 diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml new file mode 100644 index 000000000..3eed6f493 --- /dev/null +++ b/helm/gTopLevel/applyStylesheets.ml @@ -0,0 +1,109 @@ +(* 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 *) +(* 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 +;; diff --git a/helm/gTopLevel/applyStylesheets.mli b/helm/gTopLevel/applyStylesheets.mli new file mode 100644 index 000000000..e42944b86 --- /dev/null +++ b/helm/gTopLevel/applyStylesheets.mli @@ -0,0 +1,38 @@ +(* 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 *) +(* 15/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +val apply_proof_stylesheets : + Gdome.document -> explode_all:bool -> Gdome.document +val apply_sequent_stylesheets : Gdome.document -> Gdome.document diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 52f9e407f..4bef88816 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -36,7 +36,6 @@ (* GLOBAL CONSTANTS *) -let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; let htmlheader = @@ -413,89 +412,6 @@ let get_last_query = function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" ;; -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 = @@ -510,16 +426,16 @@ let 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 ;; @@ -647,9 +563,10 @@ let refresh_sequent ?(empty_notebook=true) notebook = 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 @@ -699,11 +616,9 @@ let mml_of_cic_term metano term = 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 @@ -953,7 +868,7 @@ let proveit () = (*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!!!" *) @@ -995,7 +910,7 @@ let focus () = (*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!!!" *) @@ -1908,7 +1823,7 @@ let call_tactic_with_goal_input tactic () = [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!!!" *) @@ -1965,7 +1880,7 @@ let call_tactic_with_goal_inputs tactic () = 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!!!" *) @@ -2024,7 +1939,7 @@ let call_tactic_with_input_and_goal_input tactic () = [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!!!" *) @@ -2099,7 +2014,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () = [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!!!" *) @@ -2148,7 +2063,7 @@ let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () = 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!!!" *) @@ -2180,7 +2095,7 @@ let call_tactic_with_hypothesis_input tactic () = [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!!!" *) @@ -2875,7 +2790,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = 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) diff --git a/helm/gTopLevel/misc.ml b/helm/gTopLevel/misc.ml index 139db60c8..15cd39f73 100644 --- a/helm/gTopLevel/misc.ml +++ b/helm/gTopLevel/misc.ml @@ -94,3 +94,6 @@ let wrong_xpointer_format_from_wrong_xpointer_format' uri = baseuri ^ "#" ^ rest with Not_found -> uri ;; + +let domImpl = Gdome.domImplementation ();; +let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; diff --git a/helm/gTopLevel/misc.mli b/helm/gTopLevel/misc.mli index 866976004..ac36cfdc0 100644 --- a/helm/gTopLevel/misc.mli +++ b/helm/gTopLevel/misc.mli @@ -33,9 +33,11 @@ (* *) (******************************************************************************) -(** 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 -- 2.39.2