1) Matitaweb now disambiguates scripts as it runs them

[helm.git] / matitaB / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 30bd9b83497417ef9e3737827620de485e3b0ba2..4b1bdfcc872f32cb9bcf22f4fd6b8899d6148f5c 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -57,6 +57,9 @@ class virtual status uid =
   val disambiguate_db = initial_status
   method disambiguate_db = disambiguate_db
   method set_disambiguate_db v = {< disambiguate_db = v >}
+  method reset_disambiguate_db () = 
+    {< disambiguate_db = { self#disambiguate_db with interpr =
+            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)