notation on steroids: 'term 40 x' is a valid variable name in notation and

[helm.git] / helm / software / components / grafite_parser / grafiteWalker.ml

diff --git a/helm/software/components/grafite_parser/grafiteWalker.ml b/helm/software/components/grafite_parser/grafiteWalker.ml
index eb2eb22a5ca20b4ef9e2aeec18f42f2e397ed613..7e722bccf4344c7c9f097a23892ed03733fad40a 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteWalker.ml
+++ b/helm/software/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 =
@@ -51,7 +49,8 @@ let grep_statement ?(status = LexiconEngine.initial_status) ?(callback = ignore)
     | 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
@@ -60,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
@@ -71,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)