X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcomplete_rg%2FcrgTxt.ml;h=34727aff9a28e00ea756f2eaab3aba2cbe803045;hb=da284829d696ab53dfa437e169fa669c8e58de7d;hp=267ef384f9201f678565c162024b2e0c55ddd61f;hpb=28430d599505ac26b51e4887e5196d9b380c898a;p=helm.git

diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml
index 267ef384f..34727aff9 100644
--- a/helm/software/lambda-delta/complete_rg/crgTxt.ml
+++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml
@@ -12,16 +12,17 @@
 module U  = NUri
 module H  = Hierarchy
 module C  = Cps
+module O  = Options
 module Y  = Entity
 module T  = Txt
 module TT = TxtTxt
 module D  = Crg
 
 type status = {
-   path: T.id list;          (* current section path *)
-   line: int;                (* line number *)
-   sort: int;                (* first default sort index *)
-   mk_uri:Y.uri_generator    (* uri generator *) 
+   path  : T.id list;      (* current section path *)
+   line  : int;            (* line number *)
+   sort  : int;            (* first default sort index *)
+   mk_uri: O.uri_generator (* uri generator *) 
 }
 
 let henv_size = 7000 (* hash tables initial size *)
@@ -30,10 +31,6 @@ let henv = Hashtbl.create henv_size (* optimized global environment *)
 
 (* Internal functions *******************************************************)
 
-let initial_status mk_uri = {
-   path = []; line = 1; sort = 0; mk_uri = mk_uri
-}
-
 let name_of_id ?(r=true) id = Y.Name (id, r)
 
 let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
@@ -113,7 +110,9 @@ let mk_contents tt = function
    | T.Def  -> [], Y.Abbr tt
    | T.Th   -> [], Y.Abbr tt
 
-let xlate_entity err f st = function
+let xlate_entity err f gen st = function
+   | T.Require _                  ->
+      err st
    | T.Section (Some name)        ->
       err {st with path = name :: st.path}
    | T.Section None               ->
@@ -144,10 +143,18 @@ let xlate_entity err f st = function
       let a = if meta <> "" then Y.Meta meta :: a else a in
       let entity = Y.Mark st.line :: a, uri, b in
       f {st with line = succ st.line} entity
+   | T.Generate _                 ->
+      err st
 
 (* Interface functions ******************************************************)
 
-let initial_status mk_uri =
-   initial_status mk_uri
+let initial_status () =
+   Hashtbl.clear henv; {
+   path = []; line = 1; sort = 0; mk_uri = O.get_mk_uri ()
+}
+
+let refresh_status st = {st with
+   mk_uri = O.get_mk_uri ()
+}
 
 let crg_of_txt = xlate_entity