Patch applied to the locate query: when used to retrieve the first inductive

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

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 5c6fb27d72ca260e6f931fd7ead3b24421e2d250..9dd40336a0d1f625df3ebba5d847b425efb87709 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -220,8 +220,21 @@ let locate_query s =
                        )
              )
 
-let locate s = Mqint.execute (locate_query s)
-let locate_html s = build_result (locate_query s)
+let locate s =
+ (*CSC: the code should be: Mqint.execute (locate_query s)                  *)
+ (*CSC: what follows is the patch to map mutual inductive definition blocks *)
+ (*CSC: URIs (i.e. no fragment identifier at all) to the URIs of the first  *)
+ (*CSC: mutual inductive type of their block.                               *)
+ let MQRefs uris = Mqint.execute (locate_query s) in
+  MQRefs
+   (List.map
+    (function uri ->
+      if String.sub uri (String.length uri - 4) 4 = ".con" then uri else
+       uri ^ "#1/1"
+    ) uris)
+;;
+
+let locate_html s = build_result (locate_query s);;
 
 let levels e c t =
    env := e; cont := c;