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 =
| Some (status, stm) when test stm -> (* "interesting" statement *)
let loc_begin, loc_end = HExtlib.loc_of_floc (get_loc stm) in
let raw_statement =
- String.sub content loc_begin (loc_end - loc_begin) in
+ Netconversion.ustring_sub `Enc_utf8 loc_begin (loc_end - loc_begin)
+ content in
callback raw_statement;
exaust (raw_statement :: acc) status
| Some (status, _stm) -> exaust acc status in
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
| 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)