From: Luca Padovani <luca.padovani@unito.it>
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