From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 2 Jul 2003 11:37:18 +0000 (+0000)
Subject: Bug fixed: deselecting a constraint just forgot its depth.
X-Git-Tag: camera_ready~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=19802b6487148ac232b560b43f131ffa679e4ee8;p=helm.git

Bug fixed: deselecting a constraint just forgot its depth.
---

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 6e3b846d2..aaa5f48fa 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -242,20 +242,21 @@ let add_user_constraints ~constraints
     (* to be used on "obj" *)
   let add_user_must33 user_must must =
     List.map2
-      (fun (b, i) (p, u) -> U.set_full_position p (if b then i else None), u)
-      user_must must
+     (fun (b, i) (p, u) ->
+       if b then Some (U.set_full_position p i, u) else None)
+     user_must must
   in
     (* to be used on "rel" *)
   let add_user_must22 user_must must =
     List.map2
-      (fun (b, i) p -> U.set_main_position p (if b then i else None))
-      user_must must
+     (fun (b, i) p -> if b then Some (U.set_main_position p i) else None)
+     user_must must
   in
     (* to be used on "sort" *)
   let add_user_must32 user_must must =
     List.map2
-      (fun (b, i) (p, s) -> U.set_main_position p (if b then i else None), s)
-      user_must must
+     (fun (b, i) (p, s)-> if b then Some (U.set_main_position p i, s) else None)
+     user_must must
   in
   match Pcre.split ~pat:":" constraints with
   | [user_obj;user_rel;user_sort;user_only_obj;user_only_rel;user_only_sort] ->
@@ -275,9 +276,15 @@ let add_user_constraints ~constraints
        (if user_only_sort then only_sort else None)
       in
       let must' =
-        add_user_must33 user_obj obj,
-        add_user_must22 user_rel rel,
-        add_user_must32 user_sort sort
+       let rec filter_some =
+        function
+           [] -> []
+         | None::tl -> filter_some tl
+         | (Some x)::tl -> x::(filter_some tl) 
+       in
+        filter_some (add_user_must33 user_obj obj),
+        filter_some (add_user_must22 user_rel rel),
+        filter_some (add_user_must32 user_sort sort)
       in
       (must', only')
   | _ -> failwith ("Can't parse constraint string: " ^ constraints)