let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
grafite_status#proof_status, grafite_status#moo_content_rev,
let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
grafite_status#proof_status, grafite_status#moo_content_rev,