X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=dd6c4a6f689208e76a9c4dba771790aa6a664baa;hb=4c157ac5c58f34fffc98289c2d2e71032d584a83;hp=d686c0f2c3e4abbe0476d3633eedd8b5787c0879;hpb=28430d599505ac26b51e4887e5196d9b380c898a;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index d686c0f2c..dd6c4a6f6 100644
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -12,6 +12,7 @@
 module U = NUri
 module H = U.UriHash
 module C = Cps
+module O = Options
 module Y = Entity
 module M = Meta
 module A = Aut
@@ -40,11 +41,6 @@ let hcnt = H.create hcnt_size (* optimized context *)
 
 (* Internal functions *******************************************************)
 
-let initial_status cover =
-   H.clear henv; H.clear hcnt; {
-   path = []; node = None; nodes = []; line = 1; cover = cover;
-}
-
 let id_of_name (id, _, _) = id
 
 let mk_qid st id path =
@@ -210,7 +206,13 @@ let xlate_entity err f st = function
 
 (* Interface functions ******************************************************)
 
-let initial_status ?(cover="") () =
-   initial_status cover
+let initial_status () =
+   H.clear henv; H.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; cover = !O.cover
+}
+
+let refresh_status st = {st with
+  cover = !O.cover
+}  
 
 let meta_of_aut = xlate_entity