]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/metaAut.ml
- we completed the text parser fixing the syntactic shortcuts
[helm.git] / helm / software / lambda-delta / toplevel / metaAut.ml
index d686c0f2c3e4abbe0476d3633eedd8b5787c0879..dd6c4a6f689208e76a9c4dba771790aa6a664baa 100644 (file)
@@ -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