X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteWalker.ml;h=7e722bccf4344c7c9f097a23892ed03733fad40a;hb=4a62bde42e3655a7829b9281d9b9057dc32c0471;hp=742532113894b8d6202cae4435b290886cc6f848;hpb=c780c9756b67d116b1d5b5149ae758fa613c5fe6;p=helm.git diff --git a/components/grafite_parser/grafiteWalker.ml b/components/grafite_parser/grafiteWalker.ml index 742532113..7e722bccf 100644 --- a/components/grafite_parser/grafiteWalker.ml +++ b/components/grafite_parser/grafiteWalker.ml @@ -34,10 +34,8 @@ let get_loc = loc let grep_statement ?(status = LexiconEngine.initial_status) ?(callback = ignore) - ~fname test + ~fname ~include_paths test = - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in let content = HExtlib.input_file fname in let lexbuf = Ulexing.from_utf8_string content in let parse_fun status = @@ -61,7 +59,7 @@ let grep_statement ?(status = LexiconEngine.initial_status) ?(callback = ignore) let ma_extension_test fname = Filename.check_suffix fname ".ma" let rgrep_statement ?status ?callback ?(fname_test = ma_extension_test) - ~dirname test + ~dirname ~include_paths test = let files = HExtlib.find ~test:fname_test dirname in List.flatten @@ -72,6 +70,6 @@ let rgrep_statement ?status ?callback ?(fname_test = ma_extension_test) | None -> None | Some f -> Some (fun s -> f (fname, s)) in List.map (fun raw -> fname, raw) - (grep_statement ?status ?callback ~fname test)) + (grep_statement ?status ?callback ~fname ~include_paths test)) files)