]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/complete_rg/crgTxt.ml
dr
[helm.git] / helm / software / lambda-delta / complete_rg / crgTxt.ml
index 8089c79e294d80aa9930bb147250b202b920190d..34727aff9a28e00ea756f2eaab3aba2cbe803045 100644 (file)
@@ -110,11 +110,17 @@ 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.Graph id                   ->
-      assert (H.set_graph id); err st
+   | T.Section (Some name)        ->
+      err {st with path = name :: st.path}
+   | T.Section None               ->
+      begin match st.path with
+        | _ :: ptl -> 
+           err {st with path = ptl}
+         | _        -> assert false
+      end
    | T.Sorts sorts                ->
       let map st (xix, s) =
          let ix = match xix with 
@@ -124,14 +130,8 @@ let xlate_entity err f st = function
          {st with sort = H.set_sorts ix [s]}
       in
       err (List.fold_left map st sorts)
-   | T.Section (Some name)        ->
-      err {st with path = name :: st.path}
-   | T.Section None               ->
-      begin match st.path with
-        | _ :: ptl -> 
-           err {st with path = ptl}
-         | _        -> assert false
-      end
+   | T.Graph id                   ->
+      assert (H.set_graph id); err st
    | T.Entity (kind, id, meta, t) ->
       let uri = uri_of_id st id st.path in
       Hashtbl.add henv id uri;
@@ -143,6 +143,8 @@ 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 ******************************************************)