]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: deselecting a constraint just forgot its depth.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Jul 2003 11:37:18 +0000 (11:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Jul 2003 11:37:18 +0000 (11:37 +0000)
helm/searchEngine/searchEngine.ml

index 6e3b846d2ea3ff6d6db6450e15e6aaabcc7b5ab8..aaa5f48fa34af5210bd8fd43bf2175d684bbdc98 100644 (file)
@@ -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)