diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-12 13:10:20 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-12 13:10:20 +0000 |
commit | 28ebb9d82d983e737aaf77034f1a7c4a2719396b (patch) | |
tree | 1410aef178cff5d9d4f8988e78ea47caabdd1a17 /toplevel/search.ml | |
parent | 25e9d8a825e1adc262246ae566c33efe49e8a72a (diff) |
Fixing test-suite after last storm in Pp.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/search.ml')
-rw-r--r-- | toplevel/search.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml index fbfa83d08..520b74ada 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -113,7 +113,9 @@ let xor a b = (a or b) & (not (a & b)) let plain_display accu ref a c = let pc = pr_lconstr_env a c in let pr = pr_global ref in - accu := !accu ++ hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl () + accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu + +let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l) let filter_by_module (module_list:dir_path list) (accept:bool) (ref:global_reference) _ _ = @@ -197,19 +199,19 @@ let raw_search search_function extra_filter display_function pat = ) (search_function pat) let text_pattern_search extra_filter pat = - let ans = ref (mt ()) in + let ans = ref [] in raw_search Libtypes.search_concl extra_filter (plain_display ans) pat; - !ans + format_display !ans let text_search_rewrite extra_filter pat = - let ans = ref (mt ()) in + let ans = ref [] in raw_search (Libtypes.search_eq_concl c_eq) extra_filter (plain_display ans) pat; - !ans + format_display !ans let text_search_by_head extra_filter pat = - let ans = ref (mt ()) in + let ans = ref [] in raw_search Libtypes.search_head_concl extra_filter (plain_display ans) pat; - !ans + format_display !ans let filter_by_module_from_list = function | [], _ -> (fun _ _ _ -> true) @@ -254,6 +256,6 @@ let raw_search_about filter_modules display_function l = gen_filtered_search filter display_function let search_about reference inout = - let ans = ref (mt ()) in + let ans = ref [] in raw_search_about (filter_by_module_from_list inout) (plain_display ans) reference; - !ans + format_display !ans |