]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/complete_rg/crgAut.ml
txtLexer: bug fix in parsing the string tokens
[helm.git] / helm / software / lambda-delta / complete_rg / crgAut.ml
index 8420cbea7e486b97420dff43d94064d1706229a8..0b95adf41569b16aee67026be901a4d04c6899b6 100644 (file)
@@ -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 = 
@@ -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