still commented, but benchmarks the new/old disambigution process

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b02732543b0c541504cd1d82778b5cad43fa8a1a..fbbbf6e02c450e86e335459449423e6682166918 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -571,7 +571,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
   (*
-  (match obj with
+  (let time = Unix.gettimeofday () in
+   prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
+   (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
        (try
          (match 
@@ -586,8 +588,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
            (text,prefix_len,ty)
          with
          | [_,metasenv,subst,ty],_ ->
-          prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!!  " ^
-           NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
+          let time = Unix.gettimeofday () -. time in
+          prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
+          prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
          | _ ->
           prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!!  "))
        with 
@@ -597,8 +600,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
           (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
 (*        | exn -> prerr_endline (Printexc.to_string exn) *)
        )
-    | _ -> ()
+    | _ -> ())
   ); 
+  let time = Unix.gettimeofday () in
   *)
   let (diff, metasenv, _, cic, _) =
     singleton "third"
@@ -610,6 +614,10 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
         (text,prefix_len,obj)) in
+(*
+  let time = Unix.gettimeofday () -. time in
+  prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
+*)
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic