From: Claudio Sacerdoti Coen Date: Tue, 15 May 2001 13:11:10 +0000 (+0000) Subject: **** X-Git-Tag: v0_1_3~153 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a882114fa1f2cf18f9a1ddcb83552bc29c42d95;p=helm.git **** WARNING: unstable commit **** We are just in the middle of the splitting of mmlinterface into * annotationHelper * controlInterface * proof-checker All the executables but mmlinterface are now compiling and working (but the proof-checker that is still V6-bound). --- diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml index f6d0a6a38..5b973f2ef 100644 --- a/helm/interface/getter.ml +++ b/helm/interface/getter.ml @@ -32,95 +32,8 @@ (* *) (******************************************************************************) -exception ErrorGetting of string;; -(* FEATURE MOVED TO HTTP_GETTER, Zack -module OrderedStrings = - struct - type t = string - let compare (s1 : t) (s2 : t) = compare s1 s2 - end -;; -*) - - -(* FEATURE MOVED TO HTTP_GETTER, Zack -module MapOfStrings = Map.Make(OrderedStrings);; -*) - -(* FEATURE MOVED TO HTTP_GETTER, Zack -let read_index url = - let module C = Configuration in - if Sys.command ("helm_wget " ^ C.tmp_dir ^ " " ^ url ^ "/\"" ^ - C.indexname ^ "\"") <> 0 - then - raise (ErrorGetting url) ; - let tmpfilename = C.tmp_dir ^ "/" ^ C.indexname in - let fd = open_in tmpfilename in - let uris = ref [] in - try - while true do - let (uri,comp) = - match (Str.split (Str.regexp "[ \t]+") (input_line fd)) with - [uri] -> (uri,"") - | [uri;comp] -> (uri,".gz") - in - uris := (uri,comp) :: !uris - done ; - [] (* only to make the compiler happy *) - with - End_of_file -> - Sys.remove tmpfilename ; - !uris -;; -*) - -(* FEATURE MOVED TO HTTP_GETTER, Zack -(* mk_urls_of_uris list_of_servers_base_urls *) -let rec mk_urls_of_uris = - function - [] -> MapOfStrings.empty - | he::tl -> - let map = mk_urls_of_uris tl in - let uris = read_index he in - let url_of_uri (uri,comp) = - let url = uri ^ ".xml" ^ comp in - let url' = Str.replace_first (Str.regexp "cic:") he url in - let url'' = Str.replace_first (Str.regexp "theory:") he url' in - url'' - in - List.fold_right - (fun (uri,comp) m -> MapOfStrings.add uri (url_of_uri (uri,comp)) m) - uris map -;; -*) - -exception PerlGetterNotResponding;; - -(* FEATURE MOVED TO HTTP_GETTER, Zack -let update () = - let module C = Configuration in - let fd = open_in C.servers_file in - let servers = ref [] in - try - while true do - servers := (input_line fd) :: !servers - done - with - End_of_file -> - let urls_of_uris = mk_urls_of_uris (List.rev !servers) in - (try Sys.remove (C.uris_dbm ^ ".db") with _ -> ()) ; - let dbm = - Dbm.opendbm C.uris_dbm [Dbm.Dbm_wronly ; Dbm.Dbm_create] 0o660 - in - MapOfStrings.iter (fun uri url -> Dbm.add dbm uri url) urls_of_uris ; - Dbm.close dbm ; - (* Inform also the Perl-getter *) - if Sys.command ("wget -O /dev/null http://localhost:8081/update") <> 0 - then - raise PerlGetterNotResponding ; -;; -*) +(*CSC: il getter _DEVE_ diventare un semplice "binding" a quello in Perl *) let update () = (* deliver update request to http_getter *) @@ -146,6 +59,8 @@ let name_and_ext_of_uri uri = Str.replace_first (Str.regexp ".*/") "" str ;; +let raw_get = ClientHTTP.get_and_save + (* get_file : uri -> filename *) let get_file uri = let dir = filedir_of_uri uri in @@ -153,16 +68,14 @@ let get_file uri = if not (Sys.file_exists fn) then begin let url = url_of_uri uri in - (*CSC: use -q for quiet mode *) - if Sys.command ("helm_wget " ^ dir ^ " \"" ^ url ^"\"") <> 0 - then - raise (ErrorGetting url) ; + raw_get + (Configuration.getter_url ^ "getxml?uri=" ^ + UriManager.string_of_uri uri ^ "&format=normal&patch_dtd=no" + ) fn end ; fn ;; -let raw_get = ClientHTTP.get_and_save - (* get : uri -> filename *) (* If uri is the URI of an annotation, the annotated object is processed *) let get uri = diff --git a/helm/interface/xsltProcessor.ml b/helm/interface/xsltProcessor.ml index ec3d9fdb0..95f1c70d5 100644 --- a/helm/interface/xsltProcessor.ml +++ b/helm/interface/xsltProcessor.ml @@ -23,7 +23,57 @@ * http://cs.unibo.it/helm/. *) -let initialize = XsltProcessorHTTP.initialize +let initialize () = + Printf.printf "Initializing the UWOBO servlet, please wait" ; flush stdout ; + Hashtbl.iter + (fun key uri -> + let string_to_send = (Configuration.processor_url ^ "add?xsluri=" ^ Configuration.getter_url ^ "getxslt?uri=" ^ uri ^ "&key=" ^ key) + in + print_char '.' ; flush stdout ; + ClientHTTP.send string_to_send + ) + StyleConfiguration.styles ; + Printf.printf " ok\n" ; flush stdout +;; -let process = XsltProcessorHTTP.process +(* CSC: esempio per vedere se veniva calcolata bene. Rimuovere pure il commento +http://phd.cs.unibo.it:8080/helm/servlet/uwobo/apply?xmluri=http%3A//phd.cs.unibo.it%3A8081/getxml%3Furi%3Dcic%3A/Coq/Init/Datatypes/nat_ind.con&keys=C1,C2,L¶m.processorURL=http%3A//phd.cs.unibo.it%3A8080/helm/servlet/uwobo/¶m.getterURL=http%3A//phd.cs.unibo.it%3A8081/&prop.doctype-public=&prop.encoding=&prop.media-type=text/xml¶m.doctype-public=¶m.encoding=¶m.media-type=text/xml¶m.keys=C1%2CC2%2CL¶m.CICURI=cic:/Coq/Init/Datatypes/nat_ind.con¶m.naturalLanguage=yes¶m.annotations=NO + +&keys=C1,C2,L +*) + +let process uri usecache mode naturalLanguage annotations = + let uri = UriManager.string_of_uri uri in + let url = Configuration.getter_url ^ "getxml?uri=" ^ uri in + let keys = + match StyleConfiguration.key_list_of_mode_name mode with + first_key::key_list -> + first_key ^ + (List.fold_right + (fun key cmd -> "," ^ key ^ cmd) + key_list + "" + ) + | _ -> prerr_string "Warning: the list of keys for UWOBO is empty\n"; "" + in + let string_to_send = + Configuration.processor_url ^ "apply?xmluri=" ^ url ^ + "¶m.processorURL=" ^ Configuration.processor_url ^ + "¶m.getterURL=" ^ Configuration.getter_url ^ + "&prop.doctype-public=&prop.encoding=&prop.media-type=text/xml" ^ + "&keys=" ^ keys ^ + "¶m.keys=" ^ keys ^ + "¶m.CICURI=" ^ uri ^ + "¶m.naturalLanguage=" ^ naturalLanguage ^ + "¶m.annotations=" ^ annotations ^ + "¶m.doctype-public=¶m.encoding=¶m.media-type=text/xml" + in + string_to_send +;; + +(*CSC: ma questa funzione ha senso? Se si', in quale modulo?*) +(*CSC: tutti i parametri passati alla process sono quasi a caso!!! *) +let url_of_uri uri = + process uri true "cic" "yes" "YES" +;; diff --git a/helm/interface/xsltProcessorHTTP.ml b/helm/interface/xsltProcessorHTTP.ml deleted file mode 100644 index d8f5b057e..000000000 --- a/helm/interface/xsltProcessorHTTP.ml +++ /dev/null @@ -1,55 +0,0 @@ -(* Copyright (C) 2000, 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/. - *) - -let initialize () = - Printf.printf "Initializing the UWOBO servlet, please wait" ; flush stdout ; - Hashtbl.iter - (fun key uri -> - let string_to_send = (Configuration.processor_url ^ "add?xsluri=" ^ Configuration.getter_url ^ "getxslt?uri=" ^ uri ^ "&key=" ^ key) - in - print_char '.' ; flush stdout ; - ClientHTTP.send string_to_send - ) - StyleConfiguration.styles ; - Printf.printf " ok\n" ; flush stdout -;; - -let process uri usecache mode = - let uri = UriManager.string_of_uri uri in - let url = Configuration.getter_url ^ "getxml?uri=" ^ uri in - let first_key::key_list = StyleConfiguration.key_list_of_mode_name mode in - let string_to_send = - Configuration.processor_url ^ "apply?xmluri=" ^ url ^ - "¶m.getterURL=" ^ Configuration.getter_url ^ - "&keys=" ^ first_key ^ - (List.fold_right - (fun key cmd -> "," ^ key ^ cmd) - key_list - "" - ) - in - string_to_send -;; - diff --git a/helm/interface/xsltProcessorUDP.ml b/helm/interface/xsltProcessorUDP.ml deleted file mode 100644 index a95eefc57..000000000 --- a/helm/interface/xsltProcessorUDP.ml +++ /dev/null @@ -1,93 +0,0 @@ -(* Copyright (C) 2000, 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/. - *) - -exception XsltProcessorCouldNotSend;; -exception XsltProcessorCouldNotReceive;; - -let initialize () = - Hashtbl.iter - (fun key uri -> - ignore (Sys.command ("uwobo-client add " ^ uri ^ " " ^ key)) - ) - StyleConfiguration.styles -;; - -let _ = initialize () ;; - -let portserver = 12345;; -let portclient = 12346;; -let time_to_wait = 10;; - -let rec process uri usecache mode = - let module U = Unix in - let uri = UriManager.string_of_uri uri in - let pid = string_of_int (U.getpid ()) - and filename' = - let uri' = Str.replace_first (Str.regexp ".*:") "" uri in - Str.global_replace (Str.regexp "/") "_" - (Str.global_replace (Str.regexp "_") "__" uri') - in let tmpfile = Configuration.tmp_dir ^ "/helm_" ^ filename' ^ "_" ^ pid in - (* test if the cache can be used *) - let tmp_file_exists = Sys.file_exists tmpfile in - if usecache && tmp_file_exists then - tmpfile - else - let url = Configuration.getter_url ^ uri in - (* purge the cache if asked to *) - if not usecache && tmp_file_exists then - Sys.remove tmpfile ; - (* let string_to_send = mode ^ " " ^ url ^ " " ^ tmpfile in *) - let string_to_send = "apply " ^ url ^ " " ^ tmpfile ^ - match mode with - "cic" -> " C1 C2" - | "theory" -> " T1 T2" - in - (* next function is for looping in case the server is not responding *) - let socketserver = U.socket U.PF_INET U.SOCK_DGRAM 0 in - let rec contact_server () = - let n = - U.sendto socketserver string_to_send 0 (String.length string_to_send) - [] (U.ADDR_INET(U.inet_addr_any,portserver)) - in - if n = -1 then raise XsltProcessorCouldNotSend ; - let process_signal _ = () in - Sys.set_signal Sys.sigalrm (Sys.Signal_handle process_signal) ; - (* if the server does not respond, repeat the query *) - ignore (U.alarm time_to_wait) ; - try - if U.recv socketserver "" 0 0 [] = -1 then - raise XsltProcessorCouldNotReceive ; - ignore (U.alarm 0) ; (* stop the bomb *) - Sys.set_signal Sys.sigalrm Sys.Signal_default ; - U.close socketserver ; - tmpfile - with - U.Unix_error(_,"recv",_) -> - print_endline "Xaland server not responding. Retrying..." ; - flush stdout; - contact_server () - in - contact_server () -;;