(***********************************************
TSSI: FIXME add channel stuff for universes
************************************************)
- (restore_uris v,u))
+ (restore_uris v, CicUniv.recons_graph u))
restored
;;
None ->
assert false (* only NON dummy universes can be committed *)
| Some g ->
+ CicUniv.assert_univs_have_uri g;
frozen_list := List.remove_assq uri !frozen_list ;
HT.add cacheOfCookedObjects uri (obj,g)
with
let restore_from_channel = Cache.restore_from_channel;;
let empty = Cache.empty;;
+let total_parsing_time = ref 0.0
+
let get_object_to_add uri =
let filename = Http_getter.getxml' uri in
let bodyfilename =
| None -> ()
end
in
- (* this brakes something :
- * let _ = CicUniv.restart_numbering () in
- *)
+ (* restarts the numbering of named universes (the ones inside the cic) *)
+ let _ = CicUniv.restart_numbering () in
+ (* HACK ORRIBILE: fa in modo che il parser metta degli universi fresh non
+ * anonimi *)
+ let _ = CicParser3.set_uri uri in
let obj =
try
- CicParser.obj_of_xml filename bodyfilename
+ let time = Unix.gettimeofday() in
+ let rc = CicParser.obj_of_xml filename bodyfilename in
+ total_parsing_time :=
+ !total_parsing_time +. ((Unix.gettimeofday()) -. time );
+ rc
with exn ->
cleanup ();
(match exn with