X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcomplete_rg%2FcrgAut.ml;h=0b95adf41569b16aee67026be901a4d04c6899b6;hb=2b1375e4b44e2ef351a6341a5bb0a4823e8daae5;hp=267e2b4031fa64c8b9211cd600bbf0fe725ac80a;hpb=da715664068e859d20ab81fd6969e64d58c0f57e;p=helm.git

diff --git a/helm/software/lambda-delta/complete_rg/crgAut.ml b/helm/software/lambda-delta/complete_rg/crgAut.ml
index 267e2b403..0b95adf41 100644
--- a/helm/software/lambda-delta/complete_rg/crgAut.ml
+++ b/helm/software/lambda-delta/complete_rg/crgAut.ml
@@ -12,6 +12,7 @@
 module U = NUri
 module H = U.UriHash
 module C = Cps
+module O = Options
 module Y = Entity
 module A = Aut
 module D = Crg
@@ -28,7 +29,7 @@ type status = {
    node: context_node;       (* current context node *)
    nodes: context_node list; (* context node list *)
    line: int;                (* line number *)
-   mk_uri:Y.uri_generator    (* uri generator *) 
+   mk_uri:O.uri_generator    (* uri generator *) 
 }
 
 type resolver = Local of int
@@ -42,11 +43,6 @@ let hcnt = H.create hcnt_size (* optimized context *)
 
 (* Internal functions *******************************************************)
 
-let initial_status mk_uri =
-   H.clear henv; H.clear hcnt; {
-   path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri
-}
-
 let empty_cnt = [], []
 
 let add_abst (a, ws) id w = 
@@ -62,9 +58,9 @@ let id_of_name (id, _, _) = id
 let mk_qid f st id path =
    let str = String.concat "/" path in
    let str = Filename.concat str id in 
-   let f str = f (U.uri_of_string str, id, path) in
-   f (st.mk_uri str)
-   
+   let str = st.mk_uri str in
+   f (U.uri_of_string str, id, path)
+
 let uri_of_qid (uri, _, _) = uri
 
 let complete_qid f st (id, is_local, qs) =
@@ -216,7 +212,13 @@ let xlate_entity err f st = function
 
 (* Interface functions ******************************************************)
 
-let initial_status mk_uri =
-   initial_status mk_uri
+let initial_status () =
+   H.clear henv; H.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; mk_uri = O.get_mk_uri ()
+}
+
+let refresh_status st = {st with
+   mk_uri = O.get_mk_uri ()
+}
 
 let crg_of_aut = xlate_entity