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 a211e6c1af263646604b4c45c578bf1d1da13385..1b8c3a1bd492daf5861a1e40a26cb83dcfa4a344 100644 (file)
--- 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 d79f395141c0b99ba5c8870e45836bdd14cda128..85e64117b6be0fe66366d4eaea95c811364e8617 100644 (file)
--- 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 ddb273c894b2c7cf6f1a49672e76d548070b3d65..64c068fc3b55da06d7a70dd1ff28806d6f7bc9e9 100755 (executable)
--- 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