From 2474004a0121023f37f7656289938e307b0272e7 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Sat, 17 Sep 2011 00:04:27 +0000 Subject: [PATCH] Fixes a bug (introduced in the previous revision) which caused the environment to forget its status. --- matitaB/components/ng_disambiguation/grafiteDisambiguate.ml | 4 +++- matitaB/components/ng_disambiguation/grafiteDisambiguate.mli | 1 + matitaB/components/ng_library/nCicLibrary.ml | 3 ++- matitaB/components/ng_library/nCicLibrary.mli | 1 + 4 files changed, 7 insertions(+), 2 deletions(-) diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index 3bede228d..9c7ea4768 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -48,6 +48,7 @@ let initial_status = { class type g_status = object inherit Interpretations.g_status + inherit NCicLibrary.g_status method disambiguate_db: db end @@ -63,7 +64,8 @@ class virtual status uid = DisambiguateTypes.InterprEnv.empty } >} method set_disambiguate_status : 'status. #g_status as 'status -> 'self - = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) + = fun o -> ((self#set_interp_status o)#set_disambiguate_db + o#disambiguate_db)#set_lib_status o end (* let eval_with_new_aliases status f = diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli index 640f29270..e71c25b82 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -28,6 +28,7 @@ type db class type g_status = object inherit Interpretations.g_status + inherit NCicLibrary.g_status method disambiguate_db: db end diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml index b775bff00..47a62c048 100644 --- a/matitaB/components/ng_library/nCicLibrary.ml +++ b/matitaB/components/ng_library/nCicLibrary.ml @@ -156,6 +156,7 @@ type db = { class type g_status = object + inherit NCicEnvironment.g_status method lib_db : db end @@ -175,7 +176,7 @@ class virtual status uid = method set_timestamp v = {< timestamp = v >} method set_lib_db v = {< lib_db = v >} method set_lib_status : 's.#g_status as 's -> 'self - = fun o -> {< lib_db = o#lib_db >} + = fun o -> {< lib_db = o#lib_db >}#set_env_status o end let reset_timestamp st = diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli index cba90c30c..b8453267a 100644 --- a/matitaB/components/ng_library/nCicLibrary.mli +++ b/matitaB/components/ng_library/nCicLibrary.mli @@ -20,6 +20,7 @@ type db class type g_status = object + inherit NCicEnvironment.g_status method lib_db : db end -- 2.39.2