From 7bf7eb896d5d450655d99dd78bd2a3a66b17ea1a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 14 Dec 2006 18:50:09 +0000
Subject: [PATCH] Bugged code patched, but not in the optimal way. The problem
 is that in two different interpretations a symbol id can be interpreted as
 dsc in different locations. Using the previous code it happened that every
 interpretation was pruned out since a symbol id occurred twice (in different
 locations) in an/every interpretation. Now the couples (loc,id) are
 considered for disambiguating between the two interpretations. However, this
 way we hide information to the user (what other occurrences of the same
 symbol are given the same interpretation).

---
 matita/matitaGui.ml | 37 ++++++++++++++++++++-----------------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index baf5998a5..e2a5588dc 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -1676,18 +1676,16 @@ let interactive_string_choice
     | Some uris -> uris)
 
 let interactive_interp_choice () text prefix_len choices =
-(*  List.iter (fun (l,_,_) -> 
-   List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
-   Printf.eprintf "(%d,%d)" start stop) l; prerr_endline "")
-   ((List.hd choices)); *)
+(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
  let filter_choices filter =
   let rec is_compatible filter =
    function
       [] -> true
-    | (_,id,dsc)::tl ->
+    | ([],_,_)::tl -> is_compatible filter tl
+    | (loc::tlloc,id,dsc)::tl ->
        try
-        if List.assoc id filter = dsc then
-         is_compatible filter tl
+        if List.assoc (loc,id) filter = dsc then
+         is_compatible filter ((tlloc,id,dsc)::tl)
         else
          false
        with
@@ -1695,12 +1693,14 @@ let interactive_interp_choice () text prefix_len choices =
   in
    List.filter (fun (_,interp) -> is_compatible filter interp)
  in
- let rec get_choices id =
+ let rec get_choices loc id =
   function
      [] -> []
    | (_,he)::tl ->
-      let _,_,dsc = List.find (fun (_,id',_) -> id = id') he in
-       dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices id tl))
+      let _,_,dsc =
+       List.find (fun (locs,id',_) -> id = id' && List.mem loc locs) he
+      in
+       dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices loc id tl))
  in
  let example_interp =
   match choices with
@@ -1715,19 +1715,22 @@ let interactive_interp_choice () text prefix_len choices =
  let rec classify ids filter partial_interpretations =
   match ids with
      [] -> List.map fst partial_interpretations
-   | (locs,id,_)::tl ->
-      let choices = get_choices id partial_interpretations in
+   | ([],_,_)::tl -> classify tl filter partial_interpretations
+   | (loc::tlloc,id,dsc)::tl ->
+      let choices = get_choices loc id partial_interpretations in
       let chosen_dsc =
        match choices with
-          [dsc] -> dsc
+          [] -> prerr_endline ("NO CHOICES FOR " ^ id); assert false
+        | [dsc] -> dsc
         | _ ->
-          match ask_user id locs choices with
+          match ask_user id [loc] choices with
              [x] -> x
            | _ -> assert false
       in
-      let filter = (id,chosen_dsc)::filter in
-      let compatible_interps = filter_choices filter partial_interpretations in
-       classify tl filter compatible_interps in
+       let filter = ((loc,id),chosen_dsc)::filter in
+       let compatible_interps = filter_choices filter partial_interpretations in
+        classify ((tlloc,id,dsc)::tl) filter compatible_interps
+ in
  let enumerated_choices =
   let idx = ref ~-1 in
   List.map (fun interp -> incr idx; !idx,interp) choices
-- 
2.39.2