]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter.ml
- removed some unneeded dependencies from debian/control
[helm.git] / helm / http_getter / http_getter.ml
index 48c82f8eaae356ba2f7f5218c35600b4dc1720b0..ec6564249270e627d40facb4a9af47c9670bfa95 100644 (file)
@@ -95,8 +95,11 @@ let nuprl_map = new Http_getter_map.map Http_getter_env.nuprl_dbm in
 let rdf_map = new Http_getter_map.map Http_getter_env.rdf_dbm in
 let xsl_map = new Http_getter_map.map Http_getter_env.xsl_dbm in
 
-let save_maps () =
- cic_map#close; nuprl_map#close; rdf_map#close; xsl_map#close in
+let maps = [ cic_map; nuprl_map; rdf_map; xsl_map ] in
+let close_maps () = List.iter (fun m -> m#close) maps in
+let clear_maps () = List.iter (fun m -> m#clear) maps in
+let sync_maps () = List.iter (fun m -> m#sync) maps in
+
 let map_of_uri = function
   | uri when is_cic_uri uri -> cic_map
   | uri when is_nuprl_uri uri -> nuprl_map
@@ -143,17 +146,22 @@ in
 let return_all_xml_uris = return_all_foo_uris cic_map "alluris" in
 let return_all_rdf_uris = return_all_foo_uris rdf_map "allrdfuris" in
 let return_ls =
-  let (++) (oldann, oldtypes, oldbody) (newann, newtypes, newbody) =
+  let (++) (oldann, oldtypes, oldbody, oldtree)
+           (newann, newtypes, newbody, newtree) =
     ((if newann   > oldann    then newann   else oldann),
      (if newtypes > oldtypes  then newtypes else oldtypes),
-     (if newbody  > oldbody   then newbody  else oldbody))
+     (if newbody  > oldbody   then newbody  else oldbody),
+     (if newtree  > oldtree   then newtree  else oldtree))
   in
   let basepart_RE =
-    Pcre.regexp "^([^.]*\\.[^.]*)((\\.body)|(\\.types))?(\\.ann)?"
+    Pcre.regexp
+      "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
   in
-  let (types_RE, types_ann_RE, body_RE, body_ann_RE) =
-    (Pcre.regexp "\\.types", Pcre.regexp "\\.types.ann",
-     Pcre.regexp "\\.body", Pcre.regexp "\\.body.ann")
+  let (types_RE, types_ann_RE, body_RE, body_ann_RE,
+       proof_tree_RE, proof_tree_ann_RE) =
+    (Pcre.regexp "\\.types$", Pcre.regexp "\\.types\\.ann$",
+     Pcre.regexp "\\.body$", Pcre.regexp "\\.body\\.ann$",
+     Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$")
   in
   let (slash_RE, til_slash_RE, no_slashes_RE) =
     (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
@@ -173,18 +181,22 @@ let return_ls =
     in
     let store_obj o =
       let basepart = Pcre.replace ~rex:basepart_RE ~templ:"$1" o in
+      let no_flags = false, No, No, No in
       let oldflags =
         try
           Hashtbl.find objs basepart
-        with Not_found -> (false, No, No) (* no ann, no types, no body *)
+        with Not_found -> (* no ann, no types, no body, no proof tree *)
+          no_flags
       in
       let newflags =
         match o with
-        | s when Pcre.pmatch ~rex:types_RE s     -> (false, Yes, No)
-        | s when Pcre.pmatch ~rex:types_ann_RE s -> (true,  Ann, No)
-        | s when Pcre.pmatch ~rex:body_RE s      -> (false, No,  Yes)
-        | s when Pcre.pmatch ~rex:body_ann_RE s  -> (true,  No,  Ann)
-        | s -> (false, No, No)
+        | s when Pcre.pmatch ~rex:types_RE s          -> (false, Yes, No, No)
+        | s when Pcre.pmatch ~rex:types_ann_RE s      -> (true,  Ann, No, No)
+        | s when Pcre.pmatch ~rex:body_RE s           -> (false, No, Yes, No)
+        | s when Pcre.pmatch ~rex:body_ann_RE s       -> (true,  No, Ann, No)
+        | s when Pcre.pmatch ~rex:proof_tree_RE s     -> (false, No, No, Yes)
+        | s when Pcre.pmatch ~rex:proof_tree_ann_RE s -> (true,  No, No, Ann)
+        | s -> no_flags
       in
       Hashtbl.replace objs basepart (oldflags ++ newflags)
     in
@@ -207,10 +219,12 @@ let return_ls =
             (fun s d -> sprintf "%sdir, %s\n" s d) ""
             (StringSet.elements !dirs)) ^
           (Http_getter_misc.hashtbl_sorted_fold
-            (fun uri (annflag, typesflag, bodyflag) cont ->
-              sprintf "%sobject, %s, <%s,%s,%s>\n"
+            (fun uri (annflag, typesflag, bodyflag, treeflag) cont ->
+              sprintf "%sobject, %s, <%s,%s,%s,%s>\n"
                 cont uri (if annflag then "YES" else "NO")
-                (string_of_ls_flag typesflag) (string_of_ls_flag bodyflag))
+                (string_of_ls_flag typesflag)
+                (string_of_ls_flag bodyflag)
+                (string_of_ls_flag treeflag))
             objs "")
         in
         Http_daemon.respond
@@ -234,17 +248,19 @@ let return_ls =
                 (fun d -> "<section>" ^ d ^ "</section>")
                 (StringSet.elements !dirs))) ^ "\n" ^
             (Http_getter_misc.hashtbl_sorted_fold
-              (fun uri (annflag, typesflag, bodyflag) cont ->
+              (fun uri (annflag, typesflag, bodyflag, treeflag) cont ->
                 sprintf
 "%s<object name=\"%s\">
 \t<ann value=\"%s\" />
 \t<types value=\"%s\" />
 \t<body value=\"%s\" />
+\t<proof_tree value=\"%s\" />
 </object>
 "
                   cont uri (if annflag then "YES" else "NO")
                   (string_of_ls_flag typesflag)
-                  (string_of_ls_flag bodyflag))
+                  (string_of_ls_flag bodyflag)
+                  (string_of_ls_flag treeflag))
               objs ""))
         in
         Http_daemon.respond
@@ -337,7 +353,7 @@ let update_from_server logmsg server_url = (* use global maps *)
   !log
 in
 let update_from_all_servers () =  (* use global maps *)
-  cic_map#clear; nuprl_map#clear; rdf_map#clear; xsl_map#clear;
+  clear_maps ();
   let log =
     List.fold_left
       update_from_server
@@ -345,7 +361,7 @@ let update_from_all_servers () =  (* use global maps *)
         (* reverse order: 1st server is the most important one *)
       (List.rev !Http_getter_env.servers)
   in
-  cic_map#sync; nuprl_map#sync; rdf_map#sync; xsl_map#sync;
+  sync_maps ();
   log
 in
 
@@ -510,12 +526,12 @@ let main () =
   print_string (Http_getter_env.env_to_string ());
   flush stdout;
   Unix.putenv "http_proxy" "";
-  at_exit save_maps;
+  at_exit close_maps;
   Sys.catch_break true;
   try
     Http_daemon.start'
       ~timeout:(Some 600) ~port:Http_getter_env.port ~mode:`Thread callback
-  with Sys.Break -> ()  (* 'save_maps' already registered with 'at_exit' *)
+  with Sys.Break -> ()  (* 'close_maps' already registered with 'at_exit' *)
 in
 
 main ()