The parser (the lexer indeed) now use the locate query to locate an object

[helm.git] / helm / gTopLevel / mQueryGenerator.ml

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index e08847c8fd7290b27a5a73eb43432405a5065c45..eea031f562b2bbde5d04d0d358e898a0b9a52ce7 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -167,8 +167,7 @@ let init = Mqint.init
 
 let close = Mqint.close
 
-let locate s = 
-   let query = 
+let locate_query s = 
 (*CSC: next query to be fixed
   1) I am exploiting the bug that does not quote '|'
   2) I am searching only constants and mutual inductive definition blocks
@@ -181,8 +180,9 @@ let locate s =
                              )
                        )
              )
-   in
-   build_result query
+
+let locate s = Mqint.execute (locate_query s)
+let locate_html s = build_result (locate_query s)
 
 let levels e c t level =
    env := e; cont := c;