new options activated

[helm.git] / helm / software / helena / src / text / txtCrg.ml

diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml
index 974145812ceba879cfa95be60dacedb198ffc11b..b2d0c99e1630aa54641e6cbeb1561e41ebb573ca 100644 (file)
--- a/helm/software/helena/src/text/txtCrg.ml
+++ b/helm/software/helena/src/text/txtCrg.ml
@@ -25,6 +25,7 @@ type status = {
    path  : T.id list;      (* current section path *)
    line  : int;            (* line number *)
    sort  : int;            (* first default sort index *)
+   ext   : bool;           (* extended applications *) 
    mk_uri: G.uri_generator (* uri generator *) 
 }
 
@@ -80,7 +81,7 @@ let rec xlate_term f st lenv = function
       let f _ uu = xlate_term (f uu) st lenv t in
       xlate_term f st lenv u
    | T.Appl (v, t)    ->
-      let f vv a tt = f a (D.TAppl (a, vv, tt)) in
+      let f vv a tt = f a (D.TAppl (a, st.ext, vv, tt)) in
       let f _ vv = xlate_term (f vv) st lenv t in
       xlate_term f st lenv v
    | T.Proj (bs, t)   ->
@@ -89,7 +90,7 @@ let rec xlate_term f st lenv = function
       C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
    | T.Inst (t, vs)   ->
       let map f v e =
-         let f _ vv = D.push_appl f E.empty_node vv e in
+         let f _ vv = D.push_appl f E.empty_node st.ext vv e in
          xlate_term f st lenv v
       in
       let f e a tt = f a (D.TProj (a, e, tt)) in
@@ -171,7 +172,7 @@ let xlate_entity err f gen st = function
 
 let initial_status () =
    KH.clear henv; {
-   path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
+   path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri ()
 }
 
 let refresh_status st = {st with