X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=4bef88816c302adba3a353cdaf3f1274f0f30e15;hb=7fedf47037503b281d078eef6de13927020eb410;hp=52f9e407f5e1eb93f11c8b1ef393b45d304936cd;hpb=279178e6812c3fc9d376b5e3c919d59c486d6da3;p=helm.git 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)