better tex/utf8 win

[helm.git] / helm / software / lambda-delta / toplevel / metaAut.ml

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 52aa7314dfd2aa48c945b7769e8028be956da152..5b85e46cbea703dd21fafe6f53b7242c6b5025b5 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -39,6 +39,7 @@ type status = {
    hcnt: environment;        (* optimized context *)   
    node: context_node;       (* current context node *)
    nodes: context_node list; (* context node list *)
+   line: int;                (* line number *)
    explicit: bool            (* need explicit context root? *)
 }
 
@@ -48,7 +49,7 @@ type resolver = Local of int
 let hsize = 11 (* hash tables initial size *)
 
 let initial_status size = {
-   genv = []; path = []; node = None; nodes = []; explicit = true;
+   genv = []; path = []; node = None; nodes = []; line = 1; explicit = true;
    henv = H.create size; hcnt = H.create size
 }
 
@@ -74,7 +75,7 @@ let relax_opt_qid f = function
    | None     -> f None
    | Some qid -> let f qid = f (Some qid) in relax_qid f qid
 
-let resolve_gref f st lenv gref =
+let resolve_gref f st local lenv gref =
   let rec get_local f i = function
      | []                                      -> f None
      | (name, _) :: _ when fst name = fst gref -> f (Some i)
@@ -93,14 +94,14 @@ let resolve_gref f st lenv gref =
       | Some i -> f gref (Some (Local i))
       | None   -> get_global g
   in
-  get_local f 0 lenv
+  if local then get_local f 0 lenv else f None
 
 let resolve_gref_relaxed f st lenv gref =
    let rec g gref = function
-      | None          -> relax_qid (resolve_gref g st lenv) gref
+      | None          -> relax_qid (resolve_gref g st false lenv) gref
       | Some resolved -> f gref resolved
    in
-   resolve_gref g st lenv gref
+   resolve_gref g st true lenv gref
 
 let get_pars f st = function
    | None              -> f [] None
@@ -133,10 +134,11 @@ let rec xlate_term f st lenv = function
       let f name = function
         | Local i     -> f (M.LRef i)
          | Global defs -> 
-            let map1 f = xlate_term f st lenv in
-           let map2 f (name, _) = f (M.GRef (name, [])) in
+            let l = List.length lenv in
+           let map1 f = xlate_term f st lenv in
+           let map2 f (name, _) = f (M.GRef (l, name, [])) in
             let f tail =          
-              let f args = f (M.GRef (name, args)) in
+              let f args = f (M.GRef (l, name, args)) in
                let f defs = Cps.list_rev_map_append f map2 defs ~tail in
               Cps.list_sub_strict f defs args
            in
@@ -175,9 +177,9 @@ let xlate_item f st = function
       let f pars = 
          let f name = 
             let f ww =
-              let entry = (pars, name, ww, None) in
+              let entry = (st.line, pars, name, ww, None) in
               H.add st.henv name pars;
-              f {st with genv = entry :: st.genv}
+              f {st with genv = entry :: st.genv; line = succ st.line}
            in
            xlate_term f st pars w
         in
@@ -188,9 +190,9 @@ let xlate_item f st = function
       let f pars = 
          let f name = 
             let f ww vv = 
-              let entry = (pars, name, ww, Some (trans, vv)) in
+              let entry = (st.line, pars, name, ww, Some (trans, vv)) in
               H.add st.henv name pars;
-              f {st with genv = entry :: st.genv}
+              f {st with genv = entry :: st.genv; line = succ st.line}
            in
            let f ww = xlate_term (f ww) st pars v in
            xlate_term f st pars w