From: Luca Padovani Date: Fri, 19 Jan 2001 16:15:44 +0000 (+0000) Subject: configure.in : check for perl X-Git-Tag: no-uwobo~18 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8f80848e339e75c5b6342af9a9ee91ce2d058aaa;p=helm.git configure.in : check for perl getter.ml mmlinterface.ml : patch for compressed files --- diff --git a/helm/interface/configure.in b/helm/interface/configure.in index a211e6c1a..1b8c3a1bd 100644 --- a/helm/interface/configure.in +++ b/helm/interface/configure.in @@ -21,9 +21,13 @@ fi dnl The following is the directory where the binary will be installed BIN_DIR=$RESOLVED_EXEC_PREFIX/bin +AC_PATH_PROG(PERL_BINARY,perl,no) +if test $PERL_BINARY = no ; then + AC_MSG_ERROR(Could not find perl) +fi + dnl MISSING CHECKS: -dnl ocaml, ocaml-findlib, ocaml-netstring, ocaml-pxp, lablgtk_20001129 -dnl lablgtk-20001129_gtkmathview +dnl ocaml-findlib, ocaml-netstring, ocaml-pxp dnl Check for Ocaml AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no) diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml index d79f39514..85e64117b 100644 --- a/helm/interface/getter.ml +++ b/helm/interface/getter.ml @@ -54,7 +54,12 @@ let read_index url = let uris = ref [] in try while true do - uris := (input_line fd) :: !uris + 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 @@ -70,14 +75,14 @@ let rec mk_urls_of_uris = | he::tl -> let map = mk_urls_of_uris tl in let uris = read_index he in - let url_of_uri uri = - let url = uri ^ ".xml" 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 m -> MapOfStrings.add uri (url_of_uri uri) m) + (fun (uri,comp) m -> MapOfStrings.add uri (url_of_uri (uri,comp)) m) uris map ;; diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index ddb273c89..64c068fc3 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -683,7 +683,9 @@ object(self) ignore(output#connect#selection_changed (choose_selection self)) ; ignore(nextb#connect#clicked (next self)) ; ignore(prevb#connect#clicked (prev self)) ; - ignore(checkb#connect#clicked (check self)) ; + (* LUCA: check disabled while compression is not fully implemented *) + (* ignore(checkb#connect#clicked (check self)) ; *) + checkb#misc#set_sensitive false ; ignore(closeb#connect#clicked window#misc#hide) ; ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ; let settings_window = new settings_window output scrolled_window0