open GrafiteTypes
-exception AttemptToInsertAnAlias of LexiconEngine.status
+exception AttemptToInsertAnAlias of #LexiconEngine.status
let slash_n_RE = Pcre.regexp "\\n" ;;
if Http_getter_storage.is_read_only baseuri then assert false;
activate_extraction baseuri fname ;
let lexicon_status =
- CicNotation2.load_notation ~include_paths:[]
+ CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
BuildTimeConf.core_notation_script
in
atstart (); (* FG: do not invoke before loading the core notation script *)
| [] -> grafite_status
| (g,None)::_ -> g
| (g,Some _)::_ ->
- raise (AttemptToInsertAnAlias (GrafiteTypes.get_lexicon g))
+ raise (AttemptToInsertAnAlias (GrafiteTypes.get_estatus g))
with MatitaEngine.EnrichedWithStatus
(GrafiteEngine.Macro (floc, f), grafite) as exn ->
match f (get_macro_context (Some grafite)) with
let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
grafite_status.proof_status, grafite_status.moo_content_rev,
- (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev
+ (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev
in
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
(* FG: we do not generate .moo when dumping .mma files *)
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+ NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ (GrafiteTypes.get_estatus grafite_status)#dump
end;
let tm = Unix.gmtime elapsed in
let sec = string_of_int tm.Unix.tm_sec ^ "''" in